COVID-19 update: Due to the current sanitary crisis, the school has been postponed to mid-October. 

Spring School on Theoretical Computer Science (EPIT) – Homotopy Type Theory
19-23 October 2020


The EPIT is a French thematic school proposing, on an yearly basis, an intensive 5-day long training, specializing on a particular topic in theoretical computer science. It is primarily addressed to PhD students, Post-doctoral researchers and junior academics.

The 2020 edition of the EPIT will be centered around Homotopy Type Theory, a research topic at the junction of Computer Science and Mathematics. Our hope is hence to provide an introduction that is accessible to researchers in both areas.


The school will take place at Ile d’Oléron, CAES CNRS La vieille Perrotine.


 .              Image result for anders mortberg       Image result for guillaume brunerie       Egbert Rijke

Andrej Bauer (Ljubljana University): Introduction to Homotopy Type Theory

Bas Spitters (Aarhus University): The Coq-HoTT library

Anders Mörtberg (Stockholm University): Cubical Type Theory

Guillaume Brunerie (Stockholm University): Synthetic Homotopy Theory

Egbert Rijke (Ljubljana University) : Models of Homotopy Type Theory


Paige North - CAS       

Paige North (Ohio State University): Directed Homotopy Type Theory

Valery Isaev (JetBrain, Saint Petersburg): The Arend proof assistant

Hands-on sessions

There will also be practical sessions to learn how to use various proof assistants
based on HoTT such as Cubical Agda or the Coq-HoTT library.


Comments are closed.