C. Di Giusto, MCF

Type Theory

The aim of the course is to introduce a family of formal methods to reason about programs. We will focus on type systems that are useful for statically prove the absence of some bad program behaviours.


We will introduce the main concepts on simple, recursive, and polymorphic types. We will also cover an introduction to the typed lambda calculus and subtyping.