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.

Last modified: Wed Mar 15 15:25:05 GMT 2023