⚠️ Under construction ⚠️ This website will be officialy launched with the first release of Rocq 9.0 in March 2025.
Until then, there may remain broken links and references to not-yet existing projects.
Une théorie des constructions
Thierry Coquand, PhD Thesis, Université Paris 7 — 1985
On propose une synthèse de différents systèmes de types: la théorie des types de Martin-Löf, 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)