Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstration

Collège de France - Sélection · Mar 13, 2025 · 52m

Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstration

Résumé

La théorie des types a été 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. Cette notion de types a été raffinée par la notion de type dépendant, dans le but de représenter les preuves mathématiques sur ordinateur, et de pouvoir ainsi vérifier la correction de ces preuves…