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
More Reading: Wadler (2015)
MODULE 3
Proofs
Automatic Theorem Provers
Dependent Types
More Reading: Wiedijk
MODULE 4
The Hype
Quantum Type Theory
Homotopy Type Theory
SML Bee
Tentative Guest Lecture
More Reading: Selinger (2004)
More Reading: The HoTT Book