Types

Video Recordings

Recordings of the lectures can be found on Youtube.

• The Types lecture playlist.

• 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

Slides

• 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-12.

If you are reading this then no extra material has yet been placed on the Web for this course.
Last year’s course materials are still available.

Instructions for lecturers: how to edit this page