The Coq mailing list

[nicolas tabareau <nicolas.tabareau AT inria.fr>]

====================================================================

Spring School on Theoretical Computer Science – Homotopy Type Theory (formerly EPIT2020)

The school will take place fully online, we will do our best to make it as profitable as a physical meeting.

April 12-16 2021

https://epit2020cnrs.inria.fr

====================================================================

The postponed 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.

Pre-registration is now open, please visit https://epit2020cnrs.inria.fr/registration/ <https://epit2020cnrs.inria.fr/registration/> to know more. 

For any question, please contact epit2020 AT sciencesconf.org <mailto:epit2020 AT sciencesconf.org>

As the school will be online, there is no more limitation on the number of participants, and the participation will be free. 

However, we ask you to register anyway to help us anticipate the number of people connected and choose the right infrastructure.

More details will come later. But for PhD student, we can already say that we will organize practical sessions that will 

serve as a way to validate their participation to the school, if they need to justify it to their doctoral school.

--------------------------------------------------------------------
Lecturers

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

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

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

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

Egbert Rijke (Ljubljana University): 
Synthetic Homotopy Theory

Christian Sattler (Chalmers University): 
Models of (Univalent) Type Theory

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