构造演算的强正规化
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
