2025年12月26日 (五) 16:54 imported>ExultantEditor

2025-12-26T16:54:14Z

新页面

{{For|辅酶Q|辅酶Q10}}

{{Infobox programming language
| name = Coq
| logo = [[File:Coq logo.png]]
| paradigm = [[函数式编程]]
| designer =
| developer =
| released = {{Start date and age|1989|5|1|df=yes}} (版本4.10)
| latest release version = 8.13.0<ref>{{cite web|title=Coq 8.12.2 is out|url=https://coq.inria.fr/news/coq-8-12-2-is-out.html|date=2020-12-11|access-date=2021-08-29|archive-date=2022-03-23|archive-url=https://web.archive.org/web/20220323234602/https://coq.inria.fr/news/coq-8-12-2-is-out.html}}</ref>
| latest release date = {{start date and age|2021|01|07|df=yes}}
| latest preview version = 8.13+beta1<ref>{{cite web|title=Coq 8.13+beta1 is out|url=https://coq.inria.fr/news/coq-8-13beta1-is-out.html|date=2020-12-07|access-date=2021-08-29|archive-date=2022-04-07|archive-url=https://web.archive.org/web/20220407093517/https://coq.inria.fr/news/coq-8-13beta1-is-out.html}}</ref>
| latest preview date = {{start date and age|2020|12|07|df=yes}}
| typing = [[静态类型]]，[[强类型]]
| implementations =
| dialects =
| influenced = [[Agda]]，[[Idris]], Matita, Albatross
| influenced_by = [[ML语言|ML]]（编程）<br>[[LCF]]（证明方法）<br>[[Automath]]（混合证明/编程）<br>[[System F]] 和[[直觉类型论]]
| license = [[LGPL]] 2.1
| website = {{url|http://coq.inria.fr/}}
| programming language = [[OCaml]]
| genre = {{le|证明辅助器|Proof assistant}}
| repo = {{url|https://github.com/coq/coq}}
| file ext = .v
| operating_system = [[跨平台]]
}}

[[File:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png|thumb|300px|一个交互式定理证明的CoqIDE会话，左侧为证明的脚本，右侧显示当前证明的状态。]]

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

Coq 同时还是一个[[依赖类型]]的[[函数式编程语言]]<ref>[http://coq.inria.fr/a-short-introduction-to-coq A short introduction to Coq] {{Wayback|url=http://coq.inria.fr/a-short-introduction-to-coq |date=20100812113050 }}.</ref>。它由[[法国]]PPS实验室的PI.R2团队研究开发<ref>{{Cite web |url=http://www.pps.univ-paris-diderot.fr/pi.r2/ |title=PI.R2 |accessdate=2014-01-23 |archive-date=2013-12-17 |archive-url=https://web.archive.org/web/20131217223953/http://www.pps.univ-paris-diderot.fr/pi.r2/ |dead-url=no }}</ref>，该团队由[[INRIA]]、[[巴黎综合理工学院]]、[[巴黎第十一大学]]、[[巴黎第七大学]]和[[法国国家科学研究中心]]组成。此前[[里昂高等师范学校]]亦曾参与开发。Coq 项目当前由 {{le|Gérard Huet}}、{{le|Christine Paulin-Mohring}} 和 Hugo Herbelin领导。Coq 使用 [[OCaml]] 以及少部分 [[C语言|C]] 实现。

单词 ''coq'' 在[[法语]]中意为“[[鸡|公鸡]]”，此命名体现了法国在研究活动中使用动物名称命名工具的传统。<ref>[http://flint.cs.yale.edu/cs428/coq/doc/faq.html#htoc4 Coq Version 8.0 for the Clueless (174 Hints)] {{Wayback|url=http://flint.cs.yale.edu/cs428/coq/doc/faq.html#htoc4 |date=20141122155805 }}. Flint.cs.yale.edu. Retrieved on 2013-11-07.</ref> 最初，它被简单地称作 Coc，意即构造演算（calculus of constructions）的缩写，同时也暗含了 Thierry Coquand（与 Gérard Huet 共同提出了前述的构造演算）的姓氏。

Coq 自身提供了一套规范语言 Gallina<ref>Adam Chlipala.
"Certified Programming with Dependent Types":
[http://adam.chlipala.net/cpdt/html/Universes.html "Library Universes"] {{Wayback|url=http://adam.chlipala.net/cpdt/html/Universes.html |date=20140102081433 }}.</ref>
（gallina 在[[西班牙语]]中意为“母鸡”）。使用 Gallina 书写的程序具有[[规范化性质]]——它们总是会终止。此性质使之避开了[[停机问题]]
<ref>Adam Chlipala.
"Certified Programming with Dependent Types":
[http://adam.chlipala.net/cpdt/html/GeneralRec.html "Library GeneralRec"] {{Wayback|url=http://adam.chlipala.net/cpdt/html/GeneralRec.html |date=20140102081511 }}.
[http://adam.chlipala.net/cpdt/html/InductiveTypes.html "Library InductiveTypes"] {{Wayback|url=http://adam.chlipala.net/cpdt/html/InductiveTypes.html |date=20140102081400 }}.</ref>。同时，这也使得 Coq 语言本身并非[[图灵完全]]。

== 应用 ==
* [[四色定理]]：在2004年九月使用 Coq 完成正式的证明。
* [[法伊特-汤普森定理]]：在2012年九月使用 Coq 完成正式的证明。

== 引用 ==
{{Reflist|30em}}

== 外部链接 ==
* http://coq.inria.fr/ {{Wayback|url=http://coq.inria.fr/ |date=20040825085246 }} - the official Coq English website
* https://softwarefoundations.cis.upenn.edu {{Wayback|url=https://softwarefoundations.cis.upenn.edu/ |date=20211008213108 }} - Software Foundations

{{程序设计语言|Coq}}

[[Category:程序设计语言]]
[[Category:函数式编程语言]]
[[Category:1984年建立的程式語言]]

Coq - 版本历史

2025年12月26日 (五) 16:54 imported>ExultantEditor