构造演算

构造演算(CoC)是高阶有类型 lambda 演算,这里的类型是一级值。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数,同从整数到整数的函数一样。CoC 是强规范化的。

CoC 最初由 Thierry Coquand 开发。

CoC 是 Coq 定理证明器早期版本的基础;它后来的版本建造在归纳构造演算之上,这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中,归纳数据类型必须模拟为它们的多态解构函数。