THE CALCULUS OF CONSTRUCTIONS

被引：405
作者：
COQUAND, T
HUET, G
机构：
[1] INRIA, le Chesnay, Fr, INRIA, le Chesnay, Fr
来源：
INFORMATION AND COMPUTATION | 1988年 / 76卷 / 2-3期
关键词：
COMPUTER PROGRAMMING LANGUAGES;
D O I：
10.1016/0890-5401(88)90005-3
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style. Every proof is a lambda -expression, typed with propositions of the underlying logic. By removing types we get a pure lambda -expression, expressing its associated algorithm. Computing this lambda -expression corresponds roughly to cut-elimination. It is our thesis that the Curry-Howard correspondence between propositions and types is a powerful paradigm for computer science. In the case of constructions, we obtain the notion of very high-level functioning programming language, with complex polymorphism well-suited for module specification. The notion of type encompasses the usual notion of date type, but allows as well arbitrarily complex algorithmic specifications. We develop the basic theory of a calculus of constructions, and prove a strong normalization theorem showing that all computations terminate. Finally, we suggest various extensions to stronger calculi.
引用
收藏
页码：95 / 120
页数：26
相关论文
共 48 条
  • [11] COQUAND T, 1985, LECTURE NOTES COMPUT, V203
  • [12] COQUAND T, 1986, JUN LOG COMP SCI C B
  • [13] COQUAND T, 1984, JUN INT S SEM DAT TY
  • [14] COQUAND T, 1985, IN PRESS JUL C LOG O
  • [15] Coquand T., 1985, THESIS U PARIS 7, VVII
  • [16] Curry H., 1958, COMBINATORY LOGIC, V1
  • [17] de Bruijn N. G, 1968, LECT NOTES MATH, V125, P29
  • [18] De Bruijn N. G., 1972, INDAG MATH, V34, P381, DOI DOI 10.1016/1385-7258(72)90034-0
  • [19] DEBRUIJN NG, 1980, ESSAYS COMBINATORY L
  • [20] DEBRUIJN NG, 1974, M10 INT AUT MEM
12345