Coq

维基百科,自由的百科全书
跳转至: 导航搜索
Coq
Coq logo.png
编程范型 函数式编程
发行时间 1984
最新发行时间 8.4 / 2012年8月;22個月前 (2012-08)
型態系統 静态类型强类型
啟發語言 ML and Standard ML
影響語言 Agda
作業系統 跨平台
許可證 LGPL 2.1
常用文件扩展名 .v
網站 coq.inria.fr
一个交互式定理证明的CoqIDE会话,左侧为证明的脚本,右侧显示当前证明的状态。

计算机科学中,Coq是一个定理证明辅助工具。它支持数学断言的表达式、机械化地对这些断言执行检查、辅助寻找正式证明、并从其形式化描述的构造性证明中提取出可验证的程序。Coq基于归纳构造演算构造演算的一种衍生理论之上。Coq并非一个定理机器证明语言;它提供了自动化定理证明的策略(tactics)和不同的决策过程。

Coq实现了一个依赖类型函数式编程语言[1]它是由法国PPS实验室的PI.R2团队开发的[2],该团队由INRIA巴黎综合理工学院巴黎第十一大学巴黎第七大学法国国家科学研究中心共同运营。此前在里昂高等师范学校亦有开发团队。Coq当前的项目管理为Hugo Herbelin。Coq使用OCaml实现。

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

Coq实现了Gallina,即Coq本身的规范语言。[4] 使用Gallina书写的程序具有规范化性质——它们总是会终止。这是解决停机问题的一条途径。这看来也许令人惊异,因为在其他的程序语言中无限循环(非终止)是司空见惯的。 [5]

应用[编辑]

引用[编辑]

  1. ^ A short introduction to Coq.
  2. ^ PI.R2
  3. ^ Coq Version 8.0 for the Clueless (174 Hints). Flint.cs.yale.edu. Retrieved on 2013-11-07.
  4. ^ Adam Chlipala. "Certified Programming with Dependent Types": "Library Universes".
  5. ^ Adam Chlipala. "Certified Programming with Dependent Types": "Library GeneralRec". "Library InductiveTypes".

外部链接[编辑]