Coq
脚本错误：没有“For”这个模块。
页面Module:Infobox/styles.css没有内容。
| File:Coq logo.png | |
| 编程范型 | 函数式编程 |
|---|---|
| 发行时间 | 1989年5月1日 (版本4.10) |
| 当前版本 | Template:Software version |
| 型態系統 | 静态类型，强类型 |
| 實作語言 | OCaml |
| 操作系统 | 跨平台 |
| 許可證 | LGPL 2.1 |
| 文件扩展名 | .v |
| 網站 | coq |
| 受影响于 | |
| ML（编程） LCF（证明方法） Automath（混合证明/编程） System F 和直觉类型论 | |
| 影響語言 | |
| Agda，Idris, Matita, Albatross | |
Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明中提取出可验证的（certified）程序。Coq 的理论基础是归纳构造演算（calculus of inductive constructions）、一种构造演算（calculus of constructions）的衍生理论。Coq 并非一个自动化定理机器证明语言；然而，它提供了自动化定理证明的策略（tactics）和不同的决策过程。
Coq 同时还是一个依赖类型的函数式编程语言[3]。它由法国PPS实验室的PI.R2团队研究开发[4]，该团队由INRIA、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学和法国国家科学研究中心组成。此前里昂高等师范学校亦曾参与开发。Coq 项目当前由 脚本错误：没有“ilh”这个模块。、脚本错误：没有“ilh”这个模块。 和 Hugo Herbelin领导。Coq 使用 OCaml 以及少部分 C 实现。
单词 coq 在法语中意为“公鸡”，此命名体现了法国在研究活动中使用动物名称命名工具的传统。[5] 最初，它被简单地称作 Coc，意即构造演算（calculus of constructions）的缩写，同时也暗含了 Thierry Coquand（与 Gérard Huet 共同提出了前述的构造演算）的姓氏。
Coq 自身提供了一套规范语言 Gallina[6] （gallina 在西班牙语中意为“母鸡”）。使用 Gallina 书写的程序具有规范化性质——它们总是会终止。此性质使之避开了停机问题 [7]。同时，这也使得 Coq 语言本身并非图灵完全。
应用[编辑]
引用[编辑]
- ↑ package.lua第80行Lua错误：module 'Module:Citation/CS1/Identifiers' not found
- ↑ package.lua第80行Lua错误：module 'Module:Citation/CS1/Identifiers' not found
- ↑ A short introduction to Coq （页面存档备份，存于互联网档案馆）.
- ↑ package.lua第80行Lua错误：module 'Module:Citation/CS1/Identifiers' not found
- ↑ 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
package.lua第80行Lua错误：module 'Module:Navbar/configuration' not found