Type Theory (MGS 2021)
Type Theory is at the same time an alternative to set theory as a
mathematical foundation and a programming language originally
conceived by the Swedish philosopher and mathematician Per
Martin-Löf. The course is an introduction to Type Theory which covers
the following topics:
- (Simpy typed) λ-calculus and combinatory logic
- Propositions as types
- Classical vs intuitionistic reasoning
- Dependent types, Π- and Σ-types
- Reasoning in Type Theory, Equality
- Inductive and coinductive types
- Universes and paradoxes
I will use the agda system for examples and exercises. Chapters from my
forthcoming book (The Tao of Types) will be made available to the
participants.
Lecture notes (chapters of Tao of Types):
- Simple types
- Propositional logic
- Datatypes
- Dependent types
- Predicate logic
Material from the lectures:
- Monday (intro, functions)
- whiteboard, agda
- Tuesday (sums and products, propositional logic)
- agda
- Wednesday (classical logic, inductive datatypes)
- agda (uses mylib.agda)
- Thursday (coinductive datatypes, dependent types)
- agda (uses mylib.agda)
- Friday (Dependent types, predicate logic, equality) )
- agda (uses mylib.agda), whiteboard
Exercises:
- Monday
- solutions
- Tuesday
- mylib.agda
- Wednesday
- mylib.agda has been extended!
- Thursday
- mylib.agda has been extended again!
Last modified: Fri Apr 16 10:07:21 BST 2021