#pts

文章2

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

Pure Type System 是一种用于定义依赖类型 λ 演算的通用框架。通过三元组 (S, A, R) 统一描述从简单类型到全依赖类型的各种演算。