构造演算的强正规化
摘要：构造演算（CC）是依赖类型编程和高阶构造逻辑的核心理论。最初在Coquand的1985年论文中引入，CC已经激发了25年的编程语言和类型论研究。如今，CC的扩展形成了Coq和Agda等语言的基础。本综述回顾了CC强归约性质的三个证明（即，不存在无限规约序列的良类型表达式）。它突出了证明的结构上的相似之处，同时展示了它们的区别是如何受到作者不同目标的影响的。
作者：Chris Casinghino
论文ID：2210.11240
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-10-21