Masterclass:

Introduction to Type Theory (and proof systems)

When: December 11, 2025
Where: Alsterterrasse 1, 20354 Hamburg (Germany)
Schedule: 11:00–17:00 (including an invited lunch break)
Format: In-person only'
What: Introduction to Type Theory by Thorsten Altenkirch (University of Nottingham)

Type Theory serves simultaneously as a programming language, a logic, and an alternative foundation for mathematics to Set Theory. 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.

Participation is free, but registration is required. Thanks to the generous support of the Akademie der Wissenschaften in Hamburg, we are able to provide small snacks and lunch. Unfortunately, we cannot cover travel or housing costs.

Participants:
Thorsten Altenkirch (University of Nottingham)
Andreas Avoukatos (Unviersity of Athens)
Manuel Englert (Universität Hamburg)
Björn Filter (Universität Hamburg)
Noah Giddings (TU Wien)
Hark Merkau (Universität Hamburg)
Bernhard Samtleben
Deniz Sarikaya (Vrije Universiteit Brussel & Universität zu Lübeck)
Roman Stehling (University of Hamburg)
Can Turan (University of Hamburg)

One who chose to stay not listed here

Organized by Deniz Sarikaya (Virje Universiteit Brussel & Universität zu Lübeck)

Application passed, as the event is already over : ) 

Note: For those interested in logic, there is another relevant lecture in Hamburg the following day:
“Logik und Vielfalt” by Elke Brendel (University of Bonn).
Details: https://www.awhamburg.de/veranstaltungen/aktuelle-termine/detail/vielfalt-in-der-logik.html
Maybe this helps to justify a trip to our lovely city. 

Supported by 

Die Akademie der Wissenschaften in Hamburg