Interactions of Proof Assistants and Mathematics

International Summer School, Regensburg, Germany, 2023

Important Dates

Application: May - June 9 2023
In-person registration: Aug 1 2023
Online registration: Sept 15 2023
Summer school: Sept 18-29 2023


Contact the Organizers

Program of the Summer School

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:
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) *Contributed Talks* cancelled!  

Sessions marked with * will not be streamed on Zoom.

Contributed presentations

Tue, September 19

Wednesday, September 20

Thursday, September 21

Tuesday, September 26

Thursday, September 28