Coq

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(项目)
(指南)
第23行: 第23行:
 
*[https://snapcraft.io/install/coq-prover/debian Install Coq Interactive Theorem Prover on Debian]
 
*[https://snapcraft.io/install/coq-prover/debian Install Coq Interactive Theorem Prover on Debian]
 
  sudo systemctl start snapd.service // 安装 sanpd 后要启动它
 
  sudo systemctl start snapd.service // 安装 sanpd 后要启动它
 +
* $ coqtop
 +
Welcome to Coq 8.14.0
 +
Coq <
  
 
==项目==
 
==项目==

2021年12月23日 (四) 03:30的版本

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

Coq

目录

简介

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

功能

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 <

项目

Awesome Coq Awesome.png awesome-coq

Gallina

Gallina Coq 原生的函数式编程语言

Coq包

STEM

图书

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

图集

链接

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

变换
操作
导航
工具箱