Course Notes

MODULE 1
Types
Why Type Theory / STLC
Algebraic Data Types
Montague Grammar
More Reading: Cardelli (1997)
MODULE 2
Logic
Constructive Logic
Substructural Logic
Session Types / Concurrency
More Reading: Wadler (2015)
MODULE 3
Proofs
Dependent Types
Automated Theorem Provers
Generalized Algebraic Datatypes
More Reading: Wiedijk
MODULE 4
The Hype
Quantum Type Theory
SML Bee
Homotopy Type Theory
Tentative Guest Lecture
More Reading: Selinger (2004)
More Reading: The HoTT Book