(Updated) 11 December 2025, Introduction to Type Theory by Thorsten Altenkirch (University of Nottingham)
Date: Thursday 11 December 2025
Location: Alsterterrasse 1, 20354 Hamburg [D]
Deadline: Wednesday 10 December 2025
In this course we will use the Agda system to explore the central concepts of Type Theory. Topics include dependent types, dependent functions, propositions-as-types, and formal reasoning within type theory. If time permits, we will also discuss recent developments such as Homotopy Type Theory and its implementation in Cubical Agda. This is an introductory lecture - no previous knowledge of Type Theory is required.
Registrations are accepted on a rolling basis, spots are limited.
For more information, see
https://sites.google.com/view/mc-intro-tt-by-ta/
or contact Deniz Sarikaya at d.sarikaya at uni-luebeck.de.