COVID-19 update: L'école a été décalée au 12-16 avril 2021 et sera entièrement en ligne.

Ecole de Printemps en Théorie Homotopique des Types

12-16 avril 2021

Description

L’EPIT est une école thématique française annuelle sur 5 jours, spécialisé à chaque fois sur un sujet d’informatique théorique différent. Elle est principalement adressée aux étudiant en thèse, en post-doctorat ou les jeunes académiques.

L’édition 2020 de l’EPIT sera centrée sur la théorie homotopique des types, un sujet de recherche à la frontière entre informatique et mathématique. Notre but est donc de fournir une introduction à ce sujet qui soit accessible aux chercheurs de ces deux communautés.

Localisation

L’école se déroulera entièrement en ligne. Nous ferons tout notre possible pour qu’elle soit aussi profitable qu’une école en présentiel.

Cours

 .                      

Andrej Bauer (Ljubljana University): Introduction à la théorie homotopique des types

Bas Spitters (Aarhus University): La bibliothèque Coq-HoTT

Anders Mörtberg (Stockholm University): Théorie des Types Cubiques

Egbert Rijke (Ljubljana University): Théorie de l’Homotopie Synthétique

Christian Sattler (Chalmers University): Modèles de théorie homotopique des types

Exposés

       

Paige North (Ohio State University): Théorie Homotopique Dirigée des Types

Valery Isaev (JetBrain, Saint Petersburg): L’assistant de preuve Arend

Sessions Pratiques

Il y aura aussi des sessions pratiques pour apprendre à utiliser certains assistants de preuve basés sur théorie homotopique des types comme Cubical Agda ou la bibliothèque Coq-HoTT.