主要证据
- Coq / Rocq historical notesS2 · 官方机构来源 · 官方公告
Calculus of Constructions 证明检查器开启 Coq 谱系
该系统为 Calculus of Constructions 中的证明提供机器检查，并经过持续演化成为 Coq，后更名为 Rocq。
发生了什么？
Coq/Rocq 官方历史记录显示，Thierry Coquand 与 Gérard Huet 初步实现 Calculus of Constructions 证明检查器期间，版本 1.10 于 1984 年 12 月 22 日冻结。
为什么重要？
Coq 后来承载多项重要形式化数学成果，并成为机器学习与 AI 辅助定理证明的重要环境。
重要性说明：早期 Calculus of Constructions 检查器直接发展为 Coq，建立了依赖类型证明检查这一长期用于形式数学与机械推理的平台路线。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 尚属声明
- 证据等级
- E2 · 研究记录
- AI 角色
- 仅计算支持
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 系统机械检查形式证明项；形式陈述与证明构造主要由人类提供。
- 人类贡献
- Thierry Coquand、Gérard Huet 及合作者设计类型理论并实现早期检查器。
- 验证状态
- 尚属声明 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- coq, calculus-of-constructions
- 机构
- inria
- 数学问题
- formal-proof-checking
- 方法
- dependent-type-theory, proof-checking, calculus-of-constructions
全部来源与工件
- Coq / Rocq historical notesS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-15
验证历史
- 1984-12-22 · 尚属声明 · E2 · 研究记录
官方项目历史提供了带日期的版本记录，并描述初始 Calculus of Constructions 实现。
更正
当前没有记录的更正。