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.