ECOLE DE RECHERCHE

COVID-19 update: À cause de la crise sanitaire actuelle, l'école a été décalée à 2021.

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

Dates à fixer : espérons vers le printemps 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 sur  Ile d’Oléron, au CAES CNRS La vieille Perrotine.

Cours

 .          Image result for anders mortberg      Image result for guillaume brunerie      Egbert Rijke

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

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

Egbert Rijke (Ljubljana University) : Modèles de théorie homotopique des types

Exposés

Paige North - CAS      

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.