Author(s)

Thierry Coquand

Presentation

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.

Thierry Coquand est depuis 1996 professeur en informatique à l’université de Göteborg (Suède). Récipiendaire du prix Kurt Gödel Centenary Research en 2008 pour ses recherches en logique et de l’ACM SIGPLAN Programming Languages Software Award en 2013 pour ses travaux sur les assistants de preuve, il a été professeur invité au Collège de France sur la chaire annuelle Informatique et sciences numériques, créée en partenariat avec Inria, pour l’année académique 2024-2025.

ISBN
978-2-7226-0873-3
Number in collection
336
Publication date
Language
français
Number of pages
64
Price
12.00 €
Distribution
FMSH-Diffusion
Format
Édition imprimée

Table of contents

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

Same collection

All publications from the same collection