计算机科学

首页 > 计算机科学

Coq

2018-09-05 18:11:39     所属分类:程序设计语言
Coq
Coq logo.png
编程范型 函数式编程
发行时间 1984
稳定版本
8.7.0
( 2017年10月 (2017-10)
型态系统 静态类型,强类型
操作系统 跨平台
许可证 LGPL 2.1
文件扩展名 .v
网站 coq.inria.fr
启发语言
ML(编程)
LCF(证明方法)
Automath(混合证明/编程)
System F 和直觉类型论
影响语言
Agda,Idris, Matita, Albatross
一个交互式定理证明的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 在西班牙语中意为“母鸡”)。使用 Gallina 书写的程序具有规范化性质——它们总是会终止。此性质使之避开了停机问题 [5]。同时,这也使得 Coq 语言本身并非图灵完全。

应用

  • 四色定理:在2004年九月使用 Coq 完成正式的证明。
  • 法伊特-汤普森定理:在2012年九月使用 Coq 完成正式的证明。

引用

  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".

外部链接

  • http://coq.inria.fr/ - the official Coq English website
  • http://www.cis.upenn.edu/~bcpierce/sf/ - Software Foundations

版权声明:本文由北城百科网创作,转载请联系管理获取授权,未经容许转载必究。https://www.beichengjiu.com/computerscience/340534.html

上一篇:CPL (编程语言)
下一篇:Curry
相关推荐