ECOLE DE RECHERCHE

Ecole de Printemps d’Informatique Théorique (EPIT) – Théorie Homotopique des Types
25 – 29 May 2020

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 sur  Ile d’Oléron, au CAES CNRS La vieille Perrotine.

Cours

 .           Image result for andy pitts .      Image result for anders mortberg .   .   Image result for guillaume brunerie

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

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

Andy Pitts (Cambridge University): Modèles de la théorie (univalente) des types

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

Guillaume Brunerie (Stockholm University): Théorie de l’Homotopie Synthétique

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.

 

Les commentaires sont clos.