Coq

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(简介)
(项目)
第23行: 第23行:
 
*[https://certicoq.org/ CertiCoq] A verified compiler for Coq
 
*[https://certicoq.org/ CertiCoq] A verified compiler for Coq
 
*[https://github.com/QuickChick QuickChick]
 
*[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]]
  
 
==图书==
 
==图书==

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

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

Coq

目录

简介

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

Coq 已成为跨计算机科学和数学研究的关键推动者

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

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

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

功能

指南

项目

Awesome Coq Awesome.png awesome-coq

图书

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

图集

链接

分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱