Coq

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(项目)
(项目)
(未显示1个用户的27个中间版本)
第14行: 第14行:
 
[https://coq-zh.github.io/SF-zh/lf-current/Preface.html Coq 已成为跨计算机科学和数学研究的关键推动者]
 
[https://coq-zh.github.io/SF-zh/lf-current/Preface.html Coq 已成为跨计算机科学和数学研究的关键推动者]
 
*作为一个'''编程语言的建模平台''',Coq 成为了研究员对复杂的语言定义进行描述和论证的标准工具。例如,它被用来检查 JavaCard 平台的安全性,得到了最高等级的通用准则验证,它还被用在 x86 和 [[LLVM]] 指令集以及 C 等编程语言的形式化规范中。
 
*作为一个'''编程语言的建模平台''',Coq 成为了研究员对复杂的语言定义进行描述和论证的标准工具。例如,它被用来检查 JavaCard 平台的安全性,得到了最高等级的通用准则验证,它还被用在 x86 和 [[LLVM]] 指令集以及 C 等编程语言的形式化规范中。
*作为一个'''形式化软件验证的开发环境''',Coq 被用来构建:CompCert,一个完全验证的 C 优化编译器;CertiKos,一个完全验证的工具,用于证明涉及浮点数的精妙算法的正确性;Coq 也是 CertiCrypt 的基础,一个用于论证密码学算法安全性的环境。Coq 还被用来构建开源 [[RISC]]-V 处理器架构的验证实现。
+
*作为一个'''形式化软件验证的开发环境''',Coq 被用来构建:[https://compcert.org/ CompCert] 一个完全验证的 C 优化编译器;[https://github.com/CertiKOS CertiKos] 一个完全验证的工具,用于证明涉及浮点数的精妙算法的正确性;Coq 也是 [https://github.com/EasyCrypt/certicrypt CertiCrypt] 的基础,一个用于论证密码学算法安全性的环境。Coq 还被用来构建开源 [[RISC]]-V 处理器架构的验证实现。
 
*作为一个'''依赖类型函数式编程的现实环境''',Coq 激发了大量的创新。例如 Ynot 系统嵌入了“关系式霍尔推理”(一个 '霍尔逻辑' 的扩展, 我们之后会看到它)。
 
*作为一个'''依赖类型函数式编程的现实环境''',Coq 激发了大量的创新。例如 Ynot 系统嵌入了“关系式霍尔推理”(一个 '霍尔逻辑' 的扩展, 我们之后会看到它)。
 
*作为一个'''高阶逻辑的证明助理''',Coq 被用来验证数学中一些重要的结果。例如 Coq 可在证明中包含复杂计算的能力,使其开发出了第一个形式化验证的四色定理证明。此前数学家们对该证明颇有争议,因为它需要用程序对大量组态进行检验。在 Coq 的形式化中,所有东西都被检验过,自然也包括计算的正确性。近年来,Feit-Thompson 定理经过了更大的努力用 Coq 形式化了,它是对有限单群进行分类的十分重要的第一步。
 
*作为一个'''高阶逻辑的证明助理''',Coq 被用来验证数学中一些重要的结果。例如 Coq 可在证明中包含复杂计算的能力,使其开发出了第一个形式化验证的四色定理证明。此前数学家们对该证明颇有争议,因为它需要用程序对大量组态进行检验。在 Coq 的形式化中,所有东西都被检验过,自然也包括计算的正确性。近年来,Feit-Thompson 定理经过了更大的努力用 Coq 形式化了,它是对有限单群进行分类的十分重要的第一步。
第34行: 第34行:
 
  Coq < Print positive.
 
  Coq < Print positive.
 
  Coq < Print Z.
 
  Coq < Print Z.
 +
Coq < Quit.
  
 
OPAM 安装
 
OPAM 安装
第44行: 第45行:
  
 
CoqIDE based on [[GTK]]
 
CoqIDE based on [[GTK]]
  opam search coqide
+
  $ opam search coqide
 
  # Packages matching: match(*coqide*)
 
  # Packages matching: match(*coqide*)
 
  # Name        # Installed # Synopsis
 
  # Name        # Installed # Synopsis
 
  coqide        dev        The Coq Proof Assistant --- GTK3 IDE
 
  coqide        dev        The Coq Proof Assistant --- GTK3 IDE
 
  coqide-server dev        The Coq Proof Assistant, XML protocol server
 
  coqide-server dev        The Coq Proof Assistant, XML protocol server
  > coqide
+
  $ coqide
 +
 
 +
Emacs Mode
 +
[[文件:ProofGeneral-logo.png|right|Proof General]]
 +
[https://proofgeneral.github.io/ Proof General] A generic Emacs interface for proof assistants, You can now open Coq file (.v), an EasyCrypt file (.ec), a qrhl-tool file (.qrhl), or a PhoX file (.phx).
  
 
==项目==
 
==项目==
第57行: 第62行:
 
[[文件:CertiCoq-logo.png|right|CertiCoq]]
 
[[文件:CertiCoq-logo.png|right|CertiCoq]]
 
[[文件:kami-logo.png|right|Kami]]
 
[[文件:kami-logo.png|right|Kami]]
 +
[[文件:Coq-Tezos-of-OCaml.png|right|Coq Tezos of OCaml]]
 +
[[文件:fscq-logo.png|right|FSCQ]]
 +
*[https://github.com/coq/coq Coq @ GitHub]
 
*[https://github.com/coq-community coq-community]
 
*[https://github.com/coq-community coq-community]
 
*[https://github.com/coq-contribs coq-contribs]
 
*[https://github.com/coq-contribs coq-contribs]
 +
*[https://github.com/inQWIRE/QWIRE QWIRE] a Coq implementation of the QWIRE [[量子计算|quantum]] programming language
 
*[https://github.com/math-comp Mathematical Components] [https://github.com/math-comp/fourcolor The Four Color Theorem] 四色理论
 
*[https://github.com/math-comp Mathematical Components] [https://github.com/math-comp/fourcolor The Four Color Theorem] 四色理论
 
*[https://github.com/mit-plv Programming Languages and Verification Group at MIT CSAIL]  
 
*[https://github.com/mit-plv Programming Languages and Verification Group at MIT CSAIL]  
第69行: 第78行:
 
*相似项目:[[Agda]], [[Idris]]
 
*相似项目:[[Agda]], [[Idris]]
 
*[https://certicoq.org/ CertiCoq] A verified compiler for Coq
 
*[https://certicoq.org/ CertiCoq] A verified compiler for Coq
 +
*[https://github.com/MetaCoq/metacoq MetaCoq] [[Metaprogramming]] in Coq
 
*[https://github.com/QuickChick QuickChick]
 
*[https://github.com/QuickChick QuickChick]
 
*[https://plv.csail.mit.edu/kami/ Kami]
 
*[https://plv.csail.mit.edu/kami/ Kami]
第77行: 第87行:
 
*[https://github.com/clarus/coq-chick-blog ChickBlog] A blog engine written and proven in Coq
 
*[https://github.com/clarus/coq-chick-blog ChickBlog] A blog engine written and proven in Coq
 
*[https://github.com/vellvm/vellvm Vellvm] Verifying the [[LLVM]]
 
*[https://github.com/vellvm/vellvm Vellvm] Verifying the [[LLVM]]
 +
*[https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/ Coq Tezos of OCaml] 用 Coq 翻译和验证 [[Tezos]] 经济协议的代码
 +
*[https://github.com/formal-land/coq-of-ocaml coq-of-ocaml] 可使用它做两件事:1、do formal proofs on OCaml programs; 2、port OCaml projects to Coq.
 +
*[https://github.com/plclub/hs-to-coq hs-to-coq] import [[Haskell]] to Coq
 +
*[https://github.com/tchajed/goose Goose] import [[Go]] to Coq
 +
*[https://github.com/smtcoq/smtcoq SMTCoq] Communication between Coq and SAT/SMT solvers
 +
*[http://flint.cs.yale.edu/flint/publications/feng-thesis.html An Open Framework for Certified System Software]
 +
*[https://smtcoq.github.io/ SMTCoq] Communication between Coq and SAT/SMT solvers
 +
*[https://github.com/HoTT/HoTT Homotopy Type Theory (HoTT)] 同伦类型论
 +
*[https://github.com/UniMath/UniMath Univalent Mathematics]
  
 
==语言==
 
==语言==
第84行: 第103行:
 
*[https://coq.github.io/doc/v8.9/refman/addendum/extraction.html Extraction of programs in OCaml and Haskell]
 
*[https://coq.github.io/doc/v8.9/refman/addendum/extraction.html Extraction of programs in OCaml and Haskell]
  
==Coq包==
+
==包管理==
 +
*[https://opam.ocaml.org/ opam] OCaml Package Manager
 
*[https://repology.org/project/coq/versions Packaging Coq]
 
*[https://repology.org/project/coq/versions Packaging Coq]
  
第94行: 第114行:
 
*[http://people.rennes.inria.fr/Assia.Mahboubi//cirm14.html Semantic of Proofs and Certified Mathematics]
 
*[http://people.rennes.inria.fr/Assia.Mahboubi//cirm14.html Semantic of Proofs and Certified Mathematics]
 
*[https://iris-project.org/tutorial-material.html Iris: Higher-Order Concurrent Separation Logic] Lecture Notes
 
*[https://iris-project.org/tutorial-material.html Iris: Higher-Order Concurrent Separation Logic] Lecture Notes
 +
*[https://frap.csail.mit.edu Formal Reasoning About Programs] [http://adam.chlipala.net/frap/ Adam Chlipala]
 +
*[https://www.cs.uoregon.edu/research/summerschool/summer13/curriculum.html Coq Preparation and Boot Camp] Types, Logic, and Verification
  
 
==文档==
 
==文档==
第104行: 第126行:
 
*[http://adam.chlipala.net/cpdt/ 《Certified Programming with Dependent Types》]
 
*[http://adam.chlipala.net/cpdt/ 《Certified Programming with Dependent Types》]
 
*[https://www.labri.fr/perso/casteran/CoqArt/ 《交互式定理证明与程序开发 Coq 归纳构造演算的艺术》]
 
*[https://www.labri.fr/perso/casteran/CoqArt/ 《交互式定理证明与程序开发 Coq 归纳构造演算的艺术》]
 +
*[https://math-comp.github.io/mcb/ Mathematical Components]
 +
*[https://github.com/uds-psl/MPCTT Modeling and Proving in Computational Type Theory]
 +
*[https://github.com/coq-community/hydra-battles Hydras & Co.]
 +
*[https://homotopytypetheory.org/book/ 《Homotopy Type Theory: Univalent Foundations of Mathematics》] The Univalent Foundations Program
  
 
==案例==
 
==案例==
第115行: 第141行:
 
image:coq-36-38.png|对不等式36<=38的证明
 
image:coq-36-38.png|对不等式36<=38的证明
 
image:syntax-of-propositional-logic.png|命题逻辑的符号
 
image:syntax-of-propositional-logic.png|命题逻辑的符号
 +
image:coq-of-ocaml.png|coq-of-ocaml
 +
image:A-Multipurpose-Formal-RISC-V-Specification.png|RISC-V形式化验证
 
</gallery>
 
</gallery>
  
 
==链接==
 
==链接==
 
*[https://coq.inria.fr/ Coq 官网]
 
*[https://coq.inria.fr/ Coq 官网]
*[https://github.com/coq/coq Coq @ GitHub]
+
*[https://bluespec.com/ Bluespec] Open Source RISC-V Cores and Tools
  
 +
[[category:formal]]
 
[[category:proof assistant]]
 
[[category:proof assistant]]
 
[[category:programming language]]
 
[[category:programming language]]
 
[[category:OCaml]]
 
[[category:OCaml]]
 
[[category:Huihoo Foundation]]
 
[[category:Huihoo Foundation]]

2022年10月29日 (六) 23:54的版本

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.	
Coq < Quit. 

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

Emacs Mode

Proof General

Proof General A generic Emacs interface for proof assistants, You can now open Coq file (.v), an EasyCrypt file (.ec), a qrhl-tool file (.qrhl), or a PhoX file (.phx).

项目

Awesome Coq Awesome.png awesome-coq

QuickCheck
Vellvm
CertiCoq
Kami
Coq Tezos of OCaml
FSCQ

语言

包管理

STEM

文档

图书

案例

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

图集

链接

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

变换
操作
导航
工具箱