Formalization of small imperative language ?

Stream: Is there code for X?

[Alix Trieu]

Hello, does anyone know of a formalization of a small imperative language (syntax and semantics) in Lean ?

[Henrik Böving]

Alix Trieu said:

Hello, does anyone know of a formalization of a small imperative language (syntax and semantics) in Lean ?

https://raw.githubusercontent.com/blanchette/interactive_theorem_proving_2024/main/hitchhikers_guide_2024_lmu_desktop.pdf

[Ralf Stephan]

What a great resource. :heart:

[Markus Himmel]

There is also this smaller example: https://github.com/david-christiansen/ssft24?tab=readme-ov-file#second-lecture. There is a demo at https://github.com/david-christiansen/ssft24/blob/main/Imp.lean