An Introduction to Dependent Types and Proving Your Code Correct

Long Form


This will be an introduction to dependently typed programming, the Curry-Howard correspondence, and using your type system as a proof system for showing that your code is correct all done in the programming language Agda.


Dependent typed programming languages are a very powerful framework for development. In them, we can simultaneously write our programs, write specifications for our programs, and prove our programs correct.

Agda is a powerful and mature dependently typed programming language with an excellent interactive programming mode for Emacs. This talk will be a long-form tutorial explaining the basics of dependent types, programming in Agda, and taking us through several non-trivial examples of writing data structures in Agda, encoding their properties in the types themselves, and then proving that our algorithms preserve the specified properties.

Speaking experience

I've taught courses in physics, math, and programming for almost ten years.