Coq
![]() | |
编程范型 | 函数式编程 |
---|---|
发行时间 | 1989年5月1日 | (版本4.10)
当前版本 |
|
型態系統 | 静态类型,强类型 |
實作語言 | OCaml |
操作系统 | 跨平台 |
許可證 | LGPL 2.1 |
文件扩展名 | .v |
網站 | coq |
啟發語言 | |
ML(编程) LCF(证明方法) Automath(混合证明/编程) System F 和直觉类型论 | |
影響語言 | |
Agda,Idris, Matita, Albatross |
![](http://images.weserv.nl/?url=//upload.wikimedia.org/wikipedia/commons/thumb/0/0d/CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png/300px-CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png)
Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明中提取出可验证的(certified)程序。Coq 的理论基础是归纳构造演算(calculus of inductive constructions)、一种构造演算(calculus of constructions)的衍生理论。Coq 并非一个自动化定理机器证明语言;然而,它提供了自动化定理证明的策略(tactics)和不同的决策过程。
Coq 同时还是一个依赖类型的函数式编程语言[4]。它由法国PPS实验室的PI.R2团队研究开发[5],该团队由INRIA、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学和法国国家科学研究中心组成。此前里昂高等师范学校亦曾参与开发。Coq 项目当前由 Gérard Huet、Christine Paulin-Mohring 和 Hugo Herbelin领导。Coq 使用 OCaml 以及少部分 C 实现。
单词 coq 在法语中意为“公鸡”,此命名体现了法国在研究活动中使用动物名称命名工具的传统。[6] 最初,它被简单地称作 Coc,意即构造演算(calculus of constructions)的缩写,同时也暗含了 Thierry Coquand(与 Gérard Huet 共同提出了前述的构造演算)的姓氏。
Coq 自身提供了一套规范语言 Gallina[7] (gallina 在西班牙语中意为“母鸡”)。使用 Gallina 书写的程序具有规范化性质——它们总是会终止。此性质使之避开了停机问题 [8]。同时,这也使得 Coq 语言本身并非图灵完全。
应用
引用
- ^ Release Coq 8.19.2. 2024年6月10日 [2024年7月17日].
- ^ Coq 8.12.2 is out. 2020-12-11 [2021-08-29]. (原始内容存档于2022-03-23).
- ^ Coq 8.13+beta1 is out. 2020-12-07 [2021-08-29]. (原始内容存档于2022-04-07).
- ^ A short introduction to Coq (页面存档备份,存于互联网档案馆).
- ^ PI.R2. [2014-01-23]. (原始内容存档于2013-12-17).
- ^ Coq Version 8.0 for the Clueless (174 Hints) (页面存档备份,存于互联网档案馆). Flint.cs.yale.edu. Retrieved on 2013-11-07.
- ^ Adam Chlipala. "Certified Programming with Dependent Types": "Library Universes" (页面存档备份,存于互联网档案馆).
- ^ Adam Chlipala. "Certified Programming with Dependent Types": "Library GeneralRec" (页面存档备份,存于互联网档案馆). "Library InductiveTypes" (页面存档备份,存于互联网档案馆).
外部链接
- http://coq.inria.fr/ (页面存档备份,存于互联网档案馆) - the official Coq English website
- https://softwarefoundations.cis.upenn.edu (页面存档备份,存于互联网档案馆) - Software Foundations
|