Goal
Martin-Löf Type Theory provides a powerful syntax in which to express mathematical concepts and formalise them in a programming language. Combined with Homotopy Theory, it also gives a geometric framework for proof theory that is both intuitive and helpful. The goal of this workshop is to provide an introduction to these topics for mathematicians, from type-theoretic aspects to practical implementation in a proof assistant.
Speakers
- Felix Cherubini (Augsburg).
- Tom de Jong (Nottingham).
- Maria Emilia Maietti (Padova).
- Hugo Moeneclaey (Gothenburg).
- More will be announced soon! 🎙️
Tentative schedule
The workshop will consist of two lecture series (3 x 1h) and six research talks (1h).
| Day 1 | Day 2 | Day 3 |
|---|---|---|
| Lecture A.1 | Lecture A.2 | Lecture A.3 |
| Talk 1 | Lecture B.2 | Talk 4 |
| Lunch break | Lunch break | |
| Lecture B.1 | Free afternoon | Lecture B.3 |
| Talk 2 | Talk 5 | |
| Talk 3 | Talk 6 |