CSCI-B619: Modern Dependent Types

Spring 2024

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 to engage with current research on dependent type theory and to understand the motivations behind recent extensions of these systems. Topics include extensional, intensional, homotopy, and cubical type theory.

By the end of the course, students will understand:

Research projects may naturally arise during the semester for interested students.

Meta

Location: Mondays and Wednesdays, 1:15pm–2:30pm, Ballantine Hall 006

Instructor: Carlo Angiuli, Luddy Hall 3008

Office hours: Wednesdays, 2:45pm–4:00pm, or by appointment, or when my office door is open

Syllabus: PDF (last updated 12/11/23)

Lecture notes: PDF (last updated 4/12/24)

Schedule

Date Topic Reading
Jan 8Dependent types for functional programmers§1.1
Jan 10Full-spectrum dependency, propositional equality 
Jan 15(MLK Day) 
Jan 17Simply-typed λ-calculus§2.1, PS1 out
Jan 22Simply-typed λ-calculus 
Jan 24Towards the syntax of dependent type theory§2.2, PS1 due
Jan 29The calculus of substitutions§2.3
Jan 31The calculus of substitutionsPS2 out
Feb 5Π-types, models of type theory§2.4.1
Feb 7Types internalize judgmental structure§2.4.2, PS2 due
Feb 12Σ-types, extensional equality§2.4.3, §2.4.4
Feb 14Unit, Void§2.4.5, §2.5.1, PS3 out
Feb 19Booleans, natural numbers§2.5.2, §2.5.3
Feb 21Natural numbers, unicity§2.5.4, PS3 due
Feb 26Large elimination, universes§2.6
Feb 28Universe hierarchies, type-checking§3.1
Mar 4Elaboration, normalization§3.2.1
Mar 6Bidirectionalism, consistency, canonicity§3.2.2, §3.3
Mar 11(Spring Break) 
Mar 13(Spring Break) 
Mar 18Undecidability of ETT, intro to ITT§3.4, §4.1
Mar 20Identity types (top-down perspective)PS4 out
Mar 25Identity types (bottom-up perspective)§4.2, PS5 out
Mar 27Comparing ETT and ITT§4.3, PS4 due
Apr 1Comparing ETT and ITT 
Apr 3Classifying objects§5.1
Apr 8(Solar Eclipse) 
Apr 10Classifying objects 
Apr 15Homotopy type theory§5.2
Apr 17Homotopy type theory 
Apr 22Judgmental structure for identifications§5.3
Apr 24Cubical type theory§5.4, PS5 due Friday