La théorie homotopique des types

Les assistants de preuve modernes, tels que Rocq, Lean, ou Agda, permettent de vérifier rigoureusement des preuves, qu'elles portent sur la correction de programme ou sur des objets mathématiques abstraits, afin de s'assurer de leur correction dans les moindres détails. Ces outils s'appuyent sur la théorie des types, un cadre formel qui décrit précisément les règles de la logique, et permet de s'assurer de leur cohérence. Dans ce domaine, l'une des avancées majeures des dernières décennies est l'avènement de la théorie homotopiques des types, introduite par Voevodsky, fondée sur l'intuition qu'un type doit être pensé comme un espace géométrique. Sur un plan pratique, cette approche a permis d'aboutir à un traitement plus satisfaisant de l'égalité dans les assistants de preuve. Sur le plan théorique, elle a ouvert la voie à des formalisations élégantes et générales de constructions géométriques avancées. Lors cet exposé, je présenterai les motivations et idées fondatrices de cette théorie, ainsi que certains des développements récents et pistes de recherche actuelles.

--
Ce séminaire est obligatoire pour les L3/M1 ENS informatique et ouvert aux L3 défis.