#curry-howard

文章2

本教程为读者提供一个从基础到进阶的 Pure Type System 学习路径，涵盖 PTS 核心定义、λ-Cube 谱系、构造演算 CoC、归纳构造演算 CIC，以及 Curry-Howard 同构。

CIC（Calculus of Inductive Constructions）是现代交互式定理证明器的核心理论基础。它在 CoC 的基础上增加了归纳类型，统一地表达程序、数学命题和证明。