Une théorie des constructions / Thierry Coquand ; sous la direction de G. Huet

Date :

Editeur / Publisher : [Lieu de publication inconnu] : [éditeur inconnu] , 1985

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Lambda-calcul

Isomorphisme de Curry-Howard

Théorèmes -- Démonstration automatique

Langages de programmation

Huet, Gérard (1947-.... ; informaticien) (Directeur de thèse / thesis advisor)

Université Paris Diderot - Paris 7 (1970-2019) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : On propose une synthèse de différents systèmes de types: la théorie des types de Martin-Loef, le calcul d'ordre supérieur de Girard, et le calcul automath de De Bruijn. Le résultat fondamental de ce travail est une preuve de cohérence du calcul ainsi obtenu (la théorie des constructions). D'après les résultats de Girard, ce système a la puissance d'expression de l'arithmétique d'ordre supérieure. Les exemples développes sont de deux ordres: en logique (on retrouve les différents systèmes logiques connus) et en informatique (le type étant alors la spécification du programme)