Slides and Exercises of the course "Introduction to Type Theory" at the Alfa Lernet Summer school 2008
Simple Type Theory, Curry Howard isomorphism
Simple Type Theory, principle types, normalization
Polymorphic Type Theory
Exercises for lectures 1--3
Dependent Type Theory, Logical Framewrok
Higher Order Logic, Calculus of Constructions
Exercises for lectures 4--5
References for further reading