The calculus of constructions (CC) is a core theory for dependently typed programming and higher-order constructive logic. Originally introduced in Coquand's 1985 thesis, CC has inspired 25 years of research in programming languages and type theory. Today, extensions of CC form the basis of languages like Coq and Agda. This survey reviews three proofs of CC's strong normalization property (the fact that there are no infinite reduction sequences from well-typed expressions). It highlights the similarities in the structure of the proofs while showing how their differences are motivated by the varying goals of their authors.
翻译:建筑的计算法(CC)是依附性型式编程和更高层次的建设性逻辑的核心理论。 最初在Coquand的1985年论文中引入,CC激发了25年的编程语言和类型理论研究。 今天,CC的扩展形成了Coq和Agda等语言的基础。 本调查审查了CC强大的正常化属性的三项证据(即没有从精密型式的表达方式中无限的减缩序列)。 它强调了证据结构的相似性,同时显示了其差异是如何由作者的不同目标驱动的。