Coq

来自开放百科 - 灰狐
2022年2月15日 (二) 11:49Allen (讨论 | 贡献)的版本

跳转到: 导航, 搜索
Wikipedia-35x35.png 您可以在Wikipedia上了解到此条目的英文信息 Coq Thanks, Wikipedia.

Coq

Coq

目录

简介

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

功能

Coq 是一个定理证明辅助工具,不仅可以用来开发安全应用这类需要绝对可信的程序,还可以被数学家用来开发证明。将 Coq 系统被用作一个逻辑框架,在此框架下为新的逻辑提供公理,并基于这些逻辑来开发证明。

Coq Enhancement Proposals (CEP)

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

  • 作为一个编程语言的建模平台,Coq 成为了研究员对复杂的语言定义进行描述和论证的标准工具。例如,它被用来检查 JavaCard 平台的安全性,得到了最高等级的通用准则验证,它还被用在 x86 和 LLVM 指令集以及 C 等编程语言的形式化规范中。
  • 作为一个形式化软件验证的开发环境,Coq 被用来构建:CompCert,一个完全验证的 C 优化编译器;CertiKos,一个完全验证的工具,用于证明涉及浮点数的精妙算法的正确性;Coq 也是 CertiCrypt 的基础,一个用于论证密码学算法安全性的环境。Coq 还被用来构建开源 RISC-V 处理器架构的验证实现。
  • 作为一个依赖类型函数式编程的现实环境,Coq 激发了大量的创新。例如 Ynot 系统嵌入了“关系式霍尔推理”(一个 '霍尔逻辑' 的扩展, 我们之后会看到它)。
  • 作为一个高阶逻辑的证明助理,Coq 被用来验证数学中一些重要的结果。例如 Coq 可在证明中包含复杂计算的能力,使其开发出了第一个形式化验证的四色定理证明。此前数学家们对该证明颇有争议,因为它需要用程序对大量组态进行检验。在 Coq 的形式化中,所有东西都被检验过,自然也包括计算的正确性。近年来,Feit-Thompson 定理经过了更大的努力用 Coq 形式化了,它是对有限单群进行分类的十分重要的第一步。

指南

sudo systemctl start snapd.service // 安装 sanpd 后要启动它

$ coqtop

Welcome to Coq 8.14.0
Coq < Print Scope nat_scope.
Coq 的 ZArith 库中使用的 positive 类型标识严格正整数。
Coq < Require Import ZArith.
Coq < Print positive.
Coq < Print Z.	

OPAM 安装

$ opam repository add coq-released --all-switches
$ opam install coqide
$ opam install coq-chick-blog
$ eval $(opam env)
$ coq-chick-blog
http://localhost:8008/ 

CoqIDE based on GTK

❯ opam search coqide
# Packages matching: match(*coqide*)
# Name        # Installed # Synopsis
coqide        dev         The Coq Proof Assistant --- GTK3 IDE
coqide-server dev         The Coq Proof Assistant, XML protocol server
> coqide

项目

Awesome Coq Awesome.png awesome-coq

QuickCheck
Vellvm
CertiCoq
Kami

语言

Coq包

STEM

文档

图书

案例

  • Trusted Logic 经过三年努力,成功地完成 JavaCard 语言的整个执行环境的形式化模拟。这项安全方面的工作获得 EAL7 证书奖(公共标准下最高级别的奖励)。这一形式开发工作使用了 121000 行 Coq 代码,总共 278 个模块。

图集

链接

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

变换
操作
导航
工具箱