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'
Application Deadline: asap, the places will be given out on a running basis. We expect to close application by December 1, 2025. 

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.

To apply for participation please fill out this form: 
https://forms.gle/R5q1gNCe3k8DvX8c8
We expect that most who are interested can participate but we only have 20 spaces! 

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

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