Functional Algorithms, Verified!

Stream: Program verification

[Jasmin Blanchette]

A shameless plug for the following Isabelle/HOL-based tutorial, by Nipkow et al. (including one chapter by me): Functional Algorithms, Verified!. There was an effort aiming at porting Concrete Semantics by Nipkow & Klein to Lean 3. I thought maybe this new book could have some interesting chapters for Lean 4, where the focus is shifted more towards programming.

[Kevin Cheung]

Jasmin Blanchette said:

A shameless plug for the following Isabelle/HOL-based tutorial, by Nipkow et al. (including one chapter by me): Functional Algorithms, Verified!. There was an effort aiming at porting Concrete Semantics by Nipkow & Klein to Lean 3. I thought maybe this new book could have some interesting chapters for Lean 4, where the focus is shifted more towards programming.

Has anyone started porting it to Lean 4?

[Karl Palmskog]

the Coq version might be of interest: https://github.com/clayrat/fav-ssr

[Shreyas Srinivas]

Question : Parts of the initial chapters already exist in mathlib4 and/or Std. Stuff about lists, multisets etc. Should a port repeat these proofs for completeness sake?

[Henrik Böving]

I wouldn't say so, they also make use of their stdlib, so should we. I dont think there is much of a point in a word by word replica, if it is possivle to make use of cool lean stuff we should