Modern dependent type theory

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 PDF
02 Feb 26 March 04 PDF

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:

  1. Extensional type theory
  2. Implementation and metatheory
  3. Intensional type theory
  4. Homotopy type theory
The actual exam will consist of one of these presentations (randomly selected at the beginning of the exam) along with 5–10 minutes of questions. For timing reasons, we will not offer a 30 minute review period upon selecting a topic, but students are welcome to occasionally reference notes while presenting.

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