Thierry Coquand
La Théorie des types, de Russell aux assistants à la démonstration
Ce livre retrace l’histoire récente de la théorie des types, aussi bien autour de la vérification des preuves sur ordinateur que de la synergie entre la théorie des types dépendants et la théorie de l’homotopie.
Introduite par Bertrand Russell pour éviter les paradoxes qui apparaissent en mathématique si l’on utilise de manière trop naïve la notion de collection d’objets, la théorie des types a été raffinée par la notion de type dépendant. Outre son rôle important dans la formalisation des preuves mathématiques, cette notion présente également un intérêt conceptuel intrinsèque en logique et en informatique. Ce livre retrace l’histoire récente de ces découvertes, de la vérification des preuves sur ordinateur à la synergie qui est en train de s’établir entre la théorie des types dépendants et la théorie de l’homotopie.
Coquand T., La Théorie des types, de Russell aux assistants à la démonstration, Paris, Collège de France, coll. « Leçons inaugurales », no 336, 2026, 64 p.
ISBN : 978-2-7226-0873-3
Prix : 12 €
Parution : 19 mars 2026
