CAUTION: The Sender of this email is not from within Dalhousie. ==================================================================== 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 <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/> <https://epit2020cnrs.inria.fr/registration/ <https://epit2020cnrs.inria.fr/registration/>> to know more. For any question, please contact epit2020@sciencesconf.org <mailto:epit2020@sciencesconf.org> <mailto:epit2020@sciencesconf.org <mailto:epit2020@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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]