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-02-24)

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 Towards the syntax of dependent type theory §2.2
04 Feb 26 The substitution calculus §2.3
05 Mar 04 Types and representations: Π §2.4.1, §2.4.2
06 Mar 11 Types and representations: Σ, unit, equality §2.4
07 Mar 18 Inductive types §2.5
08 Mar 25 Large elimination and universes §2.6
09 Apr 01 Proof assistants: theory and practice §3.1, §3.2
10 Apr 08 Extensional type theory has undecidable equality §3.3
11 Apr 15 The core properties of an identity type §4.1
12 Apr 22 Intensional type theory §4.2
13 Apr 29 Limitations and extensions of intensional type theory §4.3
14 May 06 Observational type theory §4.4
15 May 13 Taming universes through univalence §5.1
16 May 20 Homotopy Type Theory 2 §5
17 May 27 Homotopy Type Theory 3 §5
18 Jun 03 Homotopy Type Theory 4 §5

Problem sets

Email Daniel solutions to a problem set formatted as a PDF.

# Released on Due on Problems
01 Feb 12 Feb 19 PDF

Exam and projects

Check back later