Agda by Example: λ-calculus
If you thought that Haskell was strongly typed, think again. Languages like Agda employ a type system embodying a very powerful logic, which lets us express the meaning of our programs much more precisely. Computers can understand our programs better too, allowing for tools that are more helpful than in average languages.
In this session we will interactively develop a type checker for a simple language, then give the language semantics by embedding it into Agda. This will allow us to prove a simple optimization on the language safe, by verifying that it preserves the meaning of programs.