COVID-19 update: The school has been postponed to April 12-16 2021, and will be fully online.
Spring School on Homotopy Type Theory
April 12-16 2021
Description
The EPIT is a French thematic school proposing, on a 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.
Location
The school will take place fully online, we will do our best to make it as profitable as a physical meeting.
Lectures
.
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
Egbert Rijke (Ljubljana University): Synthetic Homotopy Theory
Christian Sattler (Chalmers University): Models of Homotopy Type Theory
Talks
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.