Coq

Coq
Coq logo.png
编程范型 函数式编程
发行时间 1984
最新发行时间 8.4pl6(2015年4月 (2015-04)
型態系統 静态类型强类型
作業系統 跨平台
許可證 LGPL 2.1
常用 文件扩展名 .v
網站 coq.inria.fr
一个交互式定理证明的CoqIDE会话,左侧为证明的脚本,右侧显示当前证明的状态。

Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的 构造性证明中提取出可验证的(certified)程序。Coq 的理论基础是 归纳构造演算(calculus of inductive constructions)、一种 构造演算(calculus of constructions)的衍生理论。Coq 并非一个自动化 定理机器证明语言;然而,它提供了自动化定理证明的策略(tactics)和不同的决策过程。

Coq 同时还是一个 依赖类型函数式编程语言 [1]。它由 法国PPS实验室的PI.R2团队研究开发 [2],该团队由 INRIA巴黎综合理工学院巴黎第十一大学巴黎第七大学法国国家科学研究中心组成。此前 里昂高等师范学校亦曾参与开发。Coq 项目当前由 Gérard Huet、Christine Paulin 和 Hugo Herbelin领导。Coq 使用 OCaml 以及少部分 C 实现。

单词 coq法语中意为" 公鸡",此命名体现了法国在研究活动中使用动物名称命名工具的传统。 [3] 最初,它被简单地称作 Coc,意即构造演算(calculus of constructions)的缩写,同时也暗含了 Thierry Coquand(与 Gérard Huet 共同提出了前述的构造演算)的姓氏。

Coq 自身提供了一套规范语言 Gallina [4] 。使用 Gallina 书写的程序具有 规范化性质——它们总是会终止。此性质使之避开了 停机问题 [5]。同时,这也使得 Coq 语言本身并非 图灵完全

应用

其他语言
Ελληνικά: Coq
English: Coq
español: Coq
suomi: Coq
français: Coq (logiciel)
日本語: Coq
русский: Coq