• Accueil
  • La théorie des types, de Russell aux assistants à la démonstration
Nouveauté

La théorie des types, de Russell aux assistants à la démonstration

Thierry COQUAND
Collection
Leçons inaugurales
Editeur
Éditions du Collège de France
Date de publication
19 mars 2026
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.
FORMAT
Livre broché
12.00 €
Ajout au panier /
Ajouter au panier
Actuellement Indisponible
Crédit
Date de première publication du titre 19 février 2026
ISBN 9782722608733
EAN-13 9782722608733
Référence 129242-07
Nombre de pages de contenu principal 64
Format 12 x 18.5 x .6 cm
Poids 78 g

1. Formalisation des mathématiques

1.1. L'apport de Russell

1.2. La logique d'ordre supérieure et le ?-calcul

1.3. AUTOMATH et la représentation des preuves sur machine

1.4. La théorie des types dépendants

1.5. Assistants de Preuve et formalisation des mathématiques

2. Analyse de la notion d'égalité en mathématique

2.1. Des lois nouvelles de l'égalité

2.2. Types comme ensemble simplicial

2.3. Le principe d'extensionalité

2.3.1. Propriété d'abstraction

2.3.2. Description définie

2.3.3. Théorie des topos d'ordre supérieur

2.4 Analyse du principe d'univalence

3. Conclusion

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.

Recommandations