International Summer School, Regensburg, Germany, 2023
All times are CEST. The conference venue is Haus der Begegnung, Hinter der Grieb 8, 93047 Regensburg: OSM
Missing lecture titles to be added.
| Monday | Tuesday | Wednesday | Thursday | Friday | |
|---|---|---|---|---|---|
| Week 1 (September 18-22) | |||||
| From 8:30: Registration |
|||||
| 9:00 - 10:30 | Yves Bertot (Slides; Examples) | Emily Riehl: Formalizing ∞-category theory in the Rzk proof assistant (Slides) | Yves Bertot (Slides, Demo 1, Demo 2, Demo 3) | John Harrison (Slides) | John Harrison (Slides) |
| Coffee break | |||||
| 11:15 - 12:00 | Introductions * | Nikolai Kudasov (rzk demo) | Paige Randall North (Notes/Exercises) | Paige Randall North (Notes/Exercises) | Angeliki Koutsoukou-Argyraki (online) (Slides) |
| Lunch break | |||||
| 14:00 - 14:45 | Tool installation, etc. * | Yves Bertot * (Demo; additional slides) | Paige Randall North (Notes/Exercises) | John Harrison (Slides) | Angeliki Koutsoukou-Argyraki (online) (Slides) |
| Coffee break | |||||
| 15:30 - 17:00 | Contributed Talks | Contributed Talks | Contributed Talks | ||
| From 19:00: Banquet at Brauhaus am Schloss * |
|||||
| Week 2 (September 25-29) | |||||
| 9:00 - 10:30 | Jannis Limperg: A Taste of Lean 4 (Material) | Benedikt Ahrens: The Univalence Principle (Slides) | Steve Awodey: Homotopical semantics for type theory (Slides) | Egbert Rijke (Agda src) | Egbert Rijke (Agda src) |
| Coffee break | |||||
| 11:15 - 12:00 | Conor McBride: Dependently typed programming as diagram completion (online) | Jannis Limperg: A Taste of Lean 4 | Thierry Coquand: From Type Theory to Homotopy Theory (online) (Slides, , A note on models) | Steve Awodey: Algebraic type theory (Slides) | Jannis Limperg: A Taste of Lean 4 Metaprogramming |
| Lunch break | |||||
| 14:00 - 14:45 | Jannis Limperg: A Taste of Lean 4 (Exercises) * | Emily Riehl/Nikolai Kudasov: Problem session | Thierry Coquand: From Type Theory to Homotopy Theory (online) (Slides) | Egbert Rijke (Agda src) | |
| Coffee break | |||||
| 15:30 - 17:00 | Michael Shulman: Modal type theories (online) (Slides, Agda src) | Contributed Talks | Leonardo de Moura (online) (Slides) |
Sessions marked with * will not be streamed on Zoom.
Tue, September 19
15:30-15:55: Cesar Bardomiano Martinez: Limits and colimits in simplicial homotopy type theory (Slides)
16:00-16:25: Matthias Hutzler: Synthetic algebraic geometry (Slides)
16:30-16:55: Sven Dziadek: Algebraic Automata Theory (Slides)
Wednesday, September 20
15:30-15:55: Florrie Verity: Pen-and-paper type theory (Slides)
16:00-16:25: Nima Rasekh: Formalising categories (Slides)
16:30-16:55: Cosimo P. Brogi: Theorem provers within theorem provers: Experiments with modal logic in HOL Light (Slides)
Thursday, September 21
15:30-15:55: David Martínez-Carpena: Limit sketches and presentability (Slides)
16:00-16:25: Jakob Rath: PolySAT – A word-level solver for large bitvectors (Slides)
16:30-16:55: Simon Guilloud: LISA: A modern proof system (Slides)
Tuesday, September 26
15:30-15:55: Matthias Uschold: Amenable groups in Lean (Slides)
16:00-16:25: Nico Beck: A language for relative category theory (Slides)
16:30-16:55: Jonas Frey: Duality for clans and dependent algebraic theories (Slides)
Thursday, September 28