This year, the course is given by Benjamin Werner and Dominik Kirst.
Sept. 18th. Introduction and motivations. Strong Normalization for simple type. First-order logic and deduction. Logical and Axiomatical Cuts in Arithmetic. Slides: handout.
Sept. 25th.
Arithmetic in Deduction Modulo. Normalization of System T. Cut Elimination in Heyting Arithmetic.
Slides: handout.
Exercises: Questions and solutions.
Oct. 2nd.
Realizability. Dependent Types.
Slides: handout.
Exercises: Questions.
Oct. 16th. Martin-Löf's Type Theory.
I had to chose youtube since you do not all have credentials for the university server I have credentials on...