登入選單

返回Google圖書搜尋

Une théorie des constructions

Thierry Coquand (professeur au Collège de France).)

出版	Éditeur inconnu, 1985
ISBN	27261041269782726104125
URL	http://books.google.com.hk/books?id=LdgWOQAACAAJ&hl=&source=gbs_api

註釋

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)