Coq

2021年12月20日 (一) 14:26的版本

您可以在Wikipedia上了解到此条目的英文信息 Coq Thanks, Wikipedia.

Coq

The Coq Proof Assistant 证明助手，使用 OCaml 编写，采用 LGPL 许可证。

作为一个编程语言的建模平台，Coq 成为了研究员对复杂的语言定义进行描述和论证的标准工具。例如，它被用来检查 JavaCard 平台的安全性，得到了最高等级的通用准则验证，它还被用在 x86 和 LLVM 指令集以及 C 等编程语言的形式化规范中。
作为一个形式化软件验证的开发环境，Coq 被用来构建：CompCert，一个完全验证的 C 优化编译器；CertiKos，一个完全验证的工具，用于证明涉及浮点数的精妙算法的正确性；

Coq 也是 CertiCrypt 的基础，一个用于论证密码学算法安全性的环境。Coq 还被用来构建开源 RISC-V 处理器架构的验证实现。

作为一个依赖类型函数式编程的现实环境，Coq 激发了大量的创新。例如 Ynot 系统嵌入了“关系式霍尔推理”（一个 '霍尔逻辑' 的扩展，我们之后会看到它）。
作为一个高阶逻辑的证明助理，Coq 被用来验证数学中一些重要的结果。例如 Coq 可在证明中包含复杂计算的能力，使其开发出了第一个形式化验证的四色定理证明。此前数学家们对该证明颇有争议，因为它需要用程序对大量组态进行检验。在 Coq 的形式化中，所有东西都被检验过，自然也包括计算的正确性。近年来，Feit-Thompson 定理经过了更大的努力用 Coq 形式化了，它是对有限单群进行分类的十分重要的第一步。

《Software Foundations》软件基础系列是对可靠软件的数学基础的广泛介绍。该系列的主要创新之处在于，每一个细节都是百分之百的形式化和机器检查：每一卷的整个文本，包括练习，实际上是Coq证明助手的 "证明脚本"。
《软件基础》系列广泛地介绍了可靠软件的数学基础，这是《Software Foundations》中文版。

@@ 第23行： / 第23行： @@
 *[https://certicoq.org/ CertiCoq] A verified compiler for Coq
 *[https://github.com/QuickChick QuickChick]
+*[https://github.com/jwiegley/coq-haskell coq-haskell] 一个在 Coq 中形式化 [[Haskell]] 类型和函数的库
+*[https://github.com/adampetcher/fcf Foundational Cryptography Framework (FCF)] [[Cryptography]]
 ==图书==