Basic information
Course decription
This is a graduate seminar 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 of this course is to prepare students with some exposure to proof assistants to engage with current research on dependent type theory. We will explore the motivations behind recent extensions of Martin-Löf type theory and cover topics such as extensional, intensional, homotopy, and cubical type theory. The course is co-taught by Lars Birkedal and Daniel Gratzer in conjunction with a sibling course at Indiana University being taught by Carlo Angiuli.
Lecture time and location
Weekly lectures take place at Monday 9:00-11:00 in Nygaard 395 (5335-395)Lecture notes
The best reference material is the accompanying lecture notes being written by Carlo Angiuli and Daniel Gratzer. These notes are work in progress and the latest public version is linked below.
Lecture Notes (Last updated 2024-04-14)Schedule
Tentative! Subject to change
| # | Date | Topic | Reading |
|---|---|---|---|
| 01 | Feb 05 | Dependent types for functional programmers | §1.1 |
| 02 | Feb 12 | Simply-typed λ-calculus | §2.1 |
| 03 | Feb 19 | Syntax and the substitution calculus | §2.2 |
| 04 | Feb 26 | The substitution calculus and Π types | §2.3, 2.4.1 |
| 05 | Mar 04 | Types and representations | §2.4.1, §2.4.2 |
| 06 | Mar 11 | Σ, Unit, and Equality types | §2.4 |
| 07 | Mar 18 | Inductive types | §2.5 |
| 08 | Mar 25 | Large elimination and universes | §2.6 |
| Apr 01 | Easter Monday | ||
| 09 | Apr 08 | Proof assistants, normalization, and consistency | §3.1, §3.2 |
| 10 | Apr 15 | Canonicity and "Eq implies undecidable type-checking" | §3.3, §3.4 |
| 11 | Apr 22 | The intensional identity type | §4.1, §4.2 |
| 12 | Apr 29 | Limitations of intensional type theory | §4.2, §4.3 |
| 13 | May 06 | Classifying objects and univalence | §5.1 |
| 14 | May 13 | Homotopy Type Theory | §5.2 |
Problem sets
Email Daniel solutions to a problem set formatted as a PDF. You are welcome to use the following starter LaTeX code to format your solutions.
| # | Released on | Due on | Problems |
|---|---|---|---|
| 01 | Feb 12 | Feb 19 | |
| 02 | Feb 26 | March 04 |
Exam and projects
There will be an oral exam on June 17 covering the material covered in the course. Students should prepare four approximately 10–15 minutes on a topic drawn from chapters 2–5. In particular:
- Extensional type theory
- Implementation and metatheory
- Intensional type theory
- Homotopy type theory
Ph.D. students in this course will complete an additional project summarizing a paper of their choice on type theory. The project is due at the end of the semester. See the project description for further information.
Talks will occur on 09:00 on Friday May 24 in Nygaard 395 (our usual meeting time and place, just on Friday). We will aim for each talk to be roughly 30 to 40 minutes plus questions. Accordingly, this will run for approximately 3 hours rather than our usual 2.
| Speaker | Paper |
|---|---|
| Egor | Definitional Proof-Irrelevance without K |
| Sergei | Axioms for Modelling Cubical Type Theory in a Topos |
| Bastien | Programming up to Congruence |
| Hei Li | Categories with Families: Unityped, Simply Typed, and Dependently Typed |
| Lasse | Constructing Quotient Inductive-Inductive Types |