EUTypes Summer School 2017

Introduction to Type Theory


This introductory course is meant to present basic notions and properties in Type Theory.

The addressed topics:

  • Untyped lambda calculus: confluence, Church numerals, expressiveness, normalization properties.
  • Simply typed lambda calculus: strong normalization, typability, Curry-Howard correspondence, inhabitation.
  • Intersection types: characterization of strong normalization, inhabitation, filter models.