Type Theory (MGS 2023)
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. Lecture notes will be made available to the
participants.
If you don't want to install agda on your computer, you can use
agdapad by Ingo
Blechschmidt.
Lecture notes (chapters of Tao of Types):
- Simple types
- Propositional logic
- Datatypes
- Dependent types
- Predicate logic
- Programs and Proofs
- Deduction
Material from the lectures:
- Sunday (intro, functions)
- agda
- Monday (sums and products, prop as types)
- agda
- Tuesday (classical logic, inductive and coinductive types)
- agda using mon-lib
- Thursday (depednent types, predicate logic, induction = recursion)
- agda using tue-lib
Exercises:
- Sunday
- Monday uses mon-lib
- Tuesday uses tue-lib
Last modified: Thu Apr 6 11:50:37 BST 2023