Going Further: mazzo.li/posts/Lambda.html
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.
* Francesco Mazzoli spent 4 years in London studying at Imperial College, where he met Haskell in his first lecture. In the past year he got interested in type theory and Agda in particular, focusing on the theme of equality for his masters’ thesis. He will soon start working at Erudify, an Haskell-backed company based in Zürich.