论文标题
构造计算的强归一化
Strong Normalization for the Calculus of Constructions
论文作者
论文摘要
构造的计算（CC）是相应地键入编程和高阶构建逻辑的核心理论。 CC最初是在Coquand的1985年论文中引入的，启发了25年的编程语言和类型理论研究。如今，CC的扩展构成了Coq和Agda等语言的基础。这项调查回顾了CC强大的归一化特性的三个证据（这一事实是，没有来自表达式的无限减少序列）。它突出了证明结构的相似之处，同时展示了他们的差异是如何由作者的不同目标激发的。
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.
