Materials for teaching type theory, used as part of the course Formal Systems and their Applications, taught at KU Leuven.
This repository contains:
- course notes on dependent type theory, to be used more or less as a plug-in chapter for TAPL (Pierce, Benjamin C. Types and programming languages. MIT press, 2002.),
- a corresponding "slider" (it's like slides, but it slides),
- a sheet explaining the Curry-Howard correspondence.