01
Pure Type
01
2026-01-05•24 min read•Uncategorized
Pure Type System 教程：从基础到进阶
本教程为读者提供一个从基础到进阶的 Pure Type System 学习路径，涵盖 PTS 核心定义、λ-Cube 谱系、构造演算 CoC、归纳构造演算 CIC，以及 Curry-Howard 同构。
类型系统PTS依赖类型
02
De Bruijn
02
2026-01-04•3 min read•Uncategorized
De Bruijn 索引：用数字代替变量名
De Bruijn 索引是一种在 lambda 演算和形式化逻辑中用于表示变量绑定的方法，它用数字代替变量名，消除了变量名冲突和 α-等价的麻烦。
类型系统λ演算形式化验证
03
CIC 理论介绍：归纳构造演算
03
2026-01-03•11 min read•Uncategorized
CIC 理论介绍：归纳构造演算
CIC（Calculus of Inductive Constructions）是现代交互式定理证明器的核心理论基础。它在 CoC 的基础上增加了归纳类型，统一地表达程序、数学命题和证明。
类型系统CIC归纳类型
04
λ-Cube：类型系统谱系
04
2026-01-02•6 min read•Uncategorized
λ-Cube：类型系统谱系
λ-Cube 由 8 个 PTS 组成，它们通过不同的规则集 R 区分，分别对应从简单类型到全依赖类型的各种演算，是理解现代证明助理理论根基的关键。
类型系统λ-Cube依赖类型
05
Pure Type
05
2026-01-01•6 min read•Uncategorized
Pure Type System (PTS) 详解
Pure Type System 是一种用于定义依赖类型 λ 演算的通用框架。通过三元组 (S, A, R) 统一描述从简单类型到全依赖类型的各种演算。
类型系统形式化验证依赖类型
5 articles in this series