Notice bibliographique
- Notice
Type(s) de contenu et mode(s) de consultation : texte noté : sans médiation
Auteur(s) : Coquand, Thierry (1961-....). Auteur du texte / Autrice du texte
Titre conventionnel : [La théorie des types, de Russell aux assistants à la démonstration (français)]
Titre(s) : La théorie des types, de Russell aux assistants à la démonstration / Thierry Coquand
Publication : Paris : Collège de France éditions, DL 2026
Impression : 14-Condé-en-Normandie : Corlet
Description matérielle : 1 volume 54 p ; 19 cm
Collection : Leçons inaugurales du Collège de France, ISSN 0294-0310 ; n° 336
Lien à la collection : Leçon inauguraleCollège de France
Note(s) : Bibliographie (9 pages)
Identifiants, prix et caractéristiques : ISBN 978-2-7226-0873-3 : 12 EUR (broché)EAN 9782722608733
Identifiant de la notice : ark:/12148/cb48743479q
Notice n° : FRBNF48743479
Résumé : 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. [source éditeur]