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: 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):

  1. Simple types
  2. Propositional logic
  3. Datatypes
  4. Dependent types
  5. Predicate logic
  6. Programs and Proofs
  7. 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