Modalités d'évaluation : lecture d'article pour l'examen partiel + examen final
Le cours tentera d'aborder les sujets suivants:
- Théorie des types de Martin-Löf
- Systèmes de types purs
- Calcul des constructions inductives
- La correspondance preuve/programme
- Types inductifs et coinductifs, codages imprédicatifs
- Extensionnalité en théorie des types
- Propriétés fondamentales: canonicité, normalisation, préservation du type par réduction, décidabilité du typage
- Conversion typée vs conversion non typée
- Paradoxes, univers
- La correspondance type/espace, égalité/chemin
- Concepts homotopiques en théorie des types (espaces contractibles, h-niveaux, univalence, discernabilité et indiscernabilité des preuves, systèmes de factorisation faible, fibrations, cofibrations)
- Type inductifs supérieurs (sphères, quotients, troncations, ...)
- Axiome du choix et logique classique en théorie des types homotopique
- Théorie des types à deux niveaux, théorie des types cubique
- Traductions internes
- Catégories de famille, modèles de préfaisceaux, modèle cubique, modèle simplicial
- ω-groupoïdes
- Complexes de Kan
Calendrier indicatif servant de ligne directrice
Merci de choisir un article dans la liste ci-dessous et d'envoyer un courrier aux enseignants pour réserver l'article. Un rapport de 2 à 5 pages sur l'article sera à rendre pour le vendredi 15 mars 2019. Un exposé oral sera à présenter le mardi 19 mars 2019.
Le rapport fera typiquement un résumé des points saillants de l'article, fera éventuellement un focus technique sur un ou plusieurs points particulièrement intéressants, etc.
- HoTT Book, 2013
- Une formalisation de HoTT en Coq
- Martin-Löf’s Type Theory, B. Nordström, K. Petersson and J. M. Smith, 2000
- Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, The Definitional Side of the Forcing, 2016.