C. Di Giusto

Type Systems

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.


  • Moodle pages
  • Types and Programming Languages. Benjamin Pierce. MIT Press 2002