Basic Information
This is a series of lectures aimed at graduate students on the modern design of full-spectrum dependent type theories, such as the core calculi of proof assistants like Agda, Coq, and Lean. The goal is to prepare students with some exposure to proof assistants to engage with current research on dependent type theory. The course is based on the textbook draft jointly written with Carlo Angiuli Principles of Dependent Type theory.
Logistics
The lectures are 90 minutes long and meet in Mondays at 13:30 in Lecture Theatre A, Wolfson Building, Parks Road. The current number of lectures is as of yet undetermined, but will proceed through the remainder of this current term with the possibility of a few bonus lectures in January.
Schedule
Tentative! Subject to change
| # | Date | Topic | Reading |
|---|---|---|---|
| 01 | Nov 04 | Dependent types for functional programmers | §1.1 |
| 02 | Nov 11 | Syntax and the substitution calculus | §2.2 and 2.3 |
| 03 | Nov 18 | Types and representations | §2.4 |
| 04 | Nov 25 | Inductive types and universes | §2.5, 2.6 |
| 05 | Dec 02 | Proof assistants, normalization, and consistency | §3.1, §3.2 |
| 06 | ?? | The intensional identity type | §4.1, §4.2 |
| 07 | ?? | Limitations of intensional type theory | §4.2, §4.3 |