This repository contains an implementation of a simple imperative language called "while" using Lean. The language has basic control structures such as conditionals, loops, and assignments.
The implementation aims to capture the semantics of the language and provide a framework for proving various properties about the language, such as termination, and correctness of various program transformations.
The implementation is grounded in the principles and techniques outlined in several books, including "Semantics with Applications: An Appetizer" by Hanne Riis Nielson and Flemming Nielson, as well as "The Formal Semantics of Programming Languages: An Introduction" by Glynn Winskel.
The "while" language has the following features:
- Integers as the only data type
- Variables and assignments
- Conditionals (if-then-else statements)
- Loops (while statements)
- Basic arithmetic operations (addition, subtraction, multiplication, and division)