Minicourse "Introduction to Type Theory"

October 8, 2025

Introduction to Type Theory
Thorsten Altenkirch (University of Nottingham)
October 27–31, 2025

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

  • λ-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
  • Homotopy Type Theory

The Agda system will be used for examples and exercises.

Timetable
Monday 27th: 16:30-18:30 - Aula G (2 hrs core lectures)
Tuesday 28th: 08:30-10:30 - Aula T.04 (2 hrs core lectures)
Wednesday 29th: 08:30-11:30 - Aula T.04 (2 hrs core lectures + 1 h supplementary lecture)
Friday 31st: 16:30-19:30 - Aula T.04 (3 hrs supplementary lectures)

Material
Link.