PrérequisLa participation aux cours d'introduction à la programmation et la preuve formelle en Coq, ou la maîtrise des notions correspondantes, est un prérequis pour ce cours.
Validationexamen
EnseignantHugo Herbelin
Horaires hebdomadaires 4 h CM
Années

Syllabus

Théorie des types de base:

  • Système de types purs
  • Théorie des types de Martin-Löf
  • Calcul des constructions inductives
  • La correspondance preuve/programme
  • Discernabilité et indiscernabilité des preuves − Types inductifs et coinductifs
  • Extensionalité en théorie des types

Théorie des types homotopique :

  • La correspondance type/espace, égalité/chemin
  • Concepts homotopiques en théorie des types (espaces contractibles, h-niveaux, univalence, systèmes de factorisation faibles, fibrations, cofibrations)
  • Type inductifs supérieurs (sphères, quotients, troncations,...)
  • Axiome du choix et logique classique en théorie des types homotopique

Modèles :

  • Catégories de famille
  • Théorie des types cubique − Traductions internes
  • ω-groupoïdes
  • Complexes de Kan

Bibliographie

  • THE UNIVALENT FOUNDATIONS PROGRAM : Homotopy type theory : Univalent foundations of mathematics (Institute for Advanced Study, 2013).