Course pages 2018–19
Lecture 1: Introduction and Review of Type Safety
Lecture 2: The Curry-Howard Correspndence
Lecture 3: Consistency and Termination
Lecture 4: Data Types and Polymorphism
Lecture 5: System F and Church Encodings
Lecture 6: Existentials, Data Abstraction, and Termination for System F
Lecture 7: Programming with State
Lecture 8: Using Monads to Control Effects
Lecture 9: Classical Logic
Lecture 10: Continuation Passing Style
Lecture 11: Applications of Continuations, and Introduction to Dependent Types
Lecture 12: The Theory of Dependent Types
Here is a set of combined slides for lectures 1-11.