coq

Coq 是一个正式的证明管理系统。它提供了一种形式语言来编写数学定义、可执行算法和定理,以及用于机器检查证明的半交互式开发的环境。典型应用包括编程语言属性的认证(例如CompCert编译器认证项目、用于验证 C 程序的Verified Software Toolchain或用于并发分离逻辑的Iris框架)、数学形式化(例如Feit的完全形式化) -汤普森定理,或同伦型理论),以及教学

参考手册和 标准库文档是 Coq 的主要文档。但是,要了解 Coq,我们建议从教程或书籍开始,例如文档页面上列出的那些。

什么是 Coq?

处理证明和程序

Coq 实现了一种名为Gallina的程序规范和数学高级语言,它基于一种名为Calculus of Inductive Constructions的表达形式语言,它本身结合了高阶逻辑和丰富类型的函数式编程语言。通过白话的命令语言,Coq 允许:

  • 定义可以有效评估的函数或谓词;
  • 陈述数学定理和软件规范;
  • 以交互方式开发这些定理的正式证明;
  • 通过相对较小的认证“内核”对这些证明进行机器检查;
  • 将经过认证的程序提取为 OCaml、Haskell 或 Scheme 等语言。

作为一个证明开发系统,Coq 提供了交互式证明方法、决策和半决策算法,以及让用户定义自己的证明方法的策略语言。可与外部计算机代数系统或定理证明器连接。

作为数学形式化或程序开发的平台,Coq 提供对高级符号、隐含内容和各种其他有用类型的宏的支持。

Coq 捆绑包

Coq 带有用于 N、Z 和 Q 中高效算术的库,关于列表、有限集和有限映射的库,关于抽象集、关系、经典分析等的库。

Coq 发布时包含:

  • 基于 gtk (CoqIDE) 的图形用户界面(参见参考手册中关于 CoqIDE 的章节),
  • 文档工具(coqdoccoq-tex)和统计工具(coqwc),
  • Coq 的依赖和 makefile 生成工具(coq_makefilecoqdep),
  • 一个独立的证明验证器(coqchk)。
学分

Coq 是 30 多年研究的成果。它始于 1984 年由 Thierry Coquand 和 Gérard Huet 在 INRIA-Rocquencourt 实施的构造微积分。1991 年,Christine Paulin 将其扩展到归纳构造微积分。总而言之,超过 200 人为 Coq 的发展做出了贡献。Coq 团队 负责 Coq 的开发和贡献的整合。有关多年来贡献者的详细列表,请参阅Coq参考手册中的历史 和最近更改章节,了解有关系统更改或合成人做了什么的详细信息 系统贡献者概览表。

Coq 是用OCaml编写的。它是根据GNU Lesser General Public License Version 2.1 (LGPL) 分发的。

分类: 默认 标签: 发布于: 2022-06-20 15:23:03, 更新于: 2022-06-20 15:26:27