CfR: 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. 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. More Information: https://sites.google.com/view/mc-intro-tt-by-ta/ 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). Questions can be send to [email protected] 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 out lovely city. Supported by Die Akademie der Wissenschaften in Hamburg -- [LOGIC] mailing list, provided by DLMPST More information (including information about subscription management) can be found here: http://dlmpst.org/pages/logic-list.php
