Abstracts.2018.CaseStudyDTP

A case study in dependently typed programming

by Ulf Norell

In traditional program verification you first write a program and then prove that it satisfies the desired properties. Correct-by-construction dependently typed programming, on the other hand, is the technique of expressing the desired properties in the type of the program itself. When done right, the extra precision in the type doesn't get in the way, and in many cases help, when writing the program. In this talk we'll write a correct-by-construction type checker for the simply typed lambda calculus, illustrating the power of dependently typed programming.

Agda code at: https://github.com/InitialTypes/Club/tree/master/lectures/stlc-typechecker