Coq Coq 是一个交互式的定理证明辅助工具它允许用户输入包含数学断言的表达式机械化地对这些断言执行检查帮助构造形式化的证明并从其形式化描述的构造性证明中提取出可验证的certified程序Coq 的理论基础是归纳构造演算calculus of inductive constructions一种构造演算calculus of constructions的衍生理论Coq 并非一个自动化定理机器证明语言然而它提供了自动化定理证明的策略tactics和不同的决策过程 Coq 同时还是一个依赖类型的函数式编程语言它由法国PPS实验室的PIR团队研究开发该团队由INRIA巴黎综合理工学院巴黎第十一大学巴黎第七大学和法国国家科学研究中心组成此前里昂高等师范学校亦曾参与开发Coq 项目当前由 Gérard Huet英语Gérard HuetChristine PaulinMohring英语Christine PaulinMohring 和 Hugo Herbelin领导Coq 使用 OCaml 以及少部分 C 实现 单词 coq 在法语中意为公鸡此命名体现了法国在研究活动中使用动物名称命名工具的传统 最初它被简单地称作 Coc意即构造演算calculus of constructions的缩写同时也暗含了 Thierry Coquand与 Gérard Huet 共同提出了前述的构造演算的姓氏 Coq 自身提供了一套规范语言 Gallina gallina 在西班牙语中意为母鸡使用 Gallina 书写的程序具有规范化性质它们总是会终止此性质使之避开了停机问题 同时这也使得 Coq 语言本身并非图灵完全