欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
Coq
来自开放百科 - 灰狐
(版本间的差异)
小 (→项目) |
小 (→STEM) |
||
(未显示1个用户的13个中间版本) | |||
第51行: | 第51行: | ||
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). | ||
==项目== | ==项目== | ||
第60行: | 第64行: | ||
[[文件:Coq-Tezos-of-OCaml.png|right|Coq Tezos of OCaml]] | [[文件:Coq-Tezos-of-OCaml.png|right|Coq Tezos of OCaml]] | ||
[[文件:fscq-logo.png|right|FSCQ]] | [[文件: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] | ||
第87行: | 第93行: | ||
*[https://github.com/smtcoq/smtcoq SMTCoq] Communication between Coq and SAT/SMT solvers | *[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] | *[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] | ||
==语言== | ==语言== | ||
第94行: | 第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] | ||
− | == | + | ==包管理== |
+ | *[https://opam.ocaml.org/ opam] OCaml Package Manager | ||
*[https://repology.org/project/coq/versions Packaging Coq] | *[https://repology.org/project/coq/versions Packaging Coq] | ||
==STEM== | ==STEM== | ||
+ | *[https://www.labri.fr/perso/casteran/CoqArt/ Tsinghua University Coq Summer School] | ||
+ | *[https://www.cs.yale.edu/flint/cs430/ CS 430/530: Formal Semantics, Fall 2013, Yale University] | ||
*[https://github.com/coq/coq/wiki/CoqInTheClassroom Coq In The Classroom] | *[https://github.com/coq/coq/wiki/CoqInTheClassroom Coq In The Classroom] | ||
*[https://fzn.fr/teaching/coq/ecole10/ Modelling and verifying algorithms in Coq] | *[https://fzn.fr/teaching/coq/ecole10/ Modelling and verifying algorithms in Coq] | ||
第116行: | 第128行: | ||
*[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 | ||
==案例== | ==案例== | ||
第128行: | 第144行: | ||
image:syntax-of-propositional-logic.png|命题逻辑的符号 | image:syntax-of-propositional-logic.png|命题逻辑的符号 | ||
image:coq-of-ocaml.png|coq-of-ocaml | 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://bluespec.com/ Bluespec] Open Source RISC-V Cores and Tools | *[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]] |
2023年4月30日 (日) 13:11的最后版本
您可以在Wikipedia上了解到此条目的英文信息 Coq Thanks, Wikipedia. |
Coq
目录 |
[编辑] 简介
The Coq Proof Assistant 证明助手,使用 OCaml 编写,采用 LGPL 许可证。
[编辑] 功能
Coq 是一个定理证明辅助工具,不仅可以用来开发安全应用这类需要绝对可信的程序,还可以被数学家用来开发证明。将 Coq 系统被用作一个逻辑框架,在此框架下为新的逻辑提供公理,并基于这些逻辑来开发证明。
Coq Enhancement Proposals (CEP)
- 作为一个编程语言的建模平台,Coq 成为了研究员对复杂的语言定义进行描述和论证的标准工具。例如,它被用来检查 JavaCard 平台的安全性,得到了最高等级的通用准则验证,它还被用在 x86 和 LLVM 指令集以及 C 等编程语言的形式化规范中。
- 作为一个形式化软件验证的开发环境,Coq 被用来构建:CompCert 一个完全验证的 C 优化编译器;CertiKos 一个完全验证的工具,用于证明涉及浮点数的精妙算法的正确性;Coq 也是 CertiCrypt 的基础,一个用于论证密码学算法安全性的环境。Coq 还被用来构建开源 RISC-V 处理器架构的验证实现。
- 作为一个依赖类型函数式编程的现实环境,Coq 激发了大量的创新。例如 Ynot 系统嵌入了“关系式霍尔推理”(一个 '霍尔逻辑' 的扩展, 我们之后会看到它)。
- 作为一个高阶逻辑的证明助理,Coq 被用来验证数学中一些重要的结果。例如 Coq 可在证明中包含复杂计算的能力,使其开发出了第一个形式化验证的四色定理证明。此前数学家们对该证明颇有争议,因为它需要用程序对大量组态进行检验。在 Coq 的形式化中,所有东西都被检验过,自然也包括计算的正确性。近年来,Feit-Thompson 定理经过了更大的努力用 Coq 形式化了,它是对有限单群进行分类的十分重要的第一步。
[编辑] 指南
- Coq Wiki
- Coq Tutorials and books
- Coq Reference Manual
- The Coq Standard Library
- Install Coq with opam 推荐
- Install Coq Interactive Theorem Prover on Debian
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 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).
[编辑] 项目
- Coq @ GitHub
- coq-community
- coq-contribs
- QWIRE a Coq implementation of the QWIRE quantum programming language
- Mathematical Components The Four Color Theorem 四色理论
- Programming Languages and Verification Group at MIT CSAIL
- Fiat-Crypto Cryptographic Primitive Code Generation by Fiat Cryptography
- Kôika A Core Language for Rule-Based Hardware Design
- Formal Reasoning About Programs 关于程序的形式化推理
- Programs and Proofs Mechanizing Mathematics with Dependent Types] 程序和证明,使用依赖类型的数学机械化
- Coq 被用于 CompCert verified C compiler CompCert验证的C编译器
- Iris 一个高阶并发分离逻辑框架,在 Coq 证明助手中实现和验证。
- 相似项目:Agda, Idris
- CertiCoq A verified compiler for Coq
- MetaCoq Metaprogramming in Coq
- QuickChick
- Kami
- coq-haskell 一个在 Coq 中形式化 Haskell 类型和函数的库
- Foundational Cryptography Framework (FCF) Cryptography
- Mtac2 A typed tactic language for Coq.
- FSCQ is a file system written and verified in the Coq proof assistant.
- ChickBlog A blog engine written and proven in Coq
- Vellvm Verifying the LLVM
- Coq Tezos of OCaml 用 Coq 翻译和验证 Tezos 经济协议的代码
- coq-of-ocaml 可使用它做两件事:1、do formal proofs on OCaml programs; 2、port OCaml projects to Coq.
- hs-to-coq import Haskell to Coq
- Goose import Go to Coq
- SMTCoq Communication between Coq and SAT/SMT solvers
- An Open Framework for Certified System Software
- SMTCoq Communication between Coq and SAT/SMT solvers
- Homotopy Type Theory (HoTT) 同伦类型论
- Univalent Mathematics
[编辑] 语言
- Gallina Coq 原生的函数式编程语言
- tactic language
- SSReflect proof language
- Extraction of programs in OCaml and Haskell
[编辑] 包管理
- opam OCaml Package Manager
- Packaging Coq
[编辑] STEM
- Tsinghua University Coq Summer School
- CS 430/530: Formal Semantics, Fall 2013, Yale University
- Coq In The Classroom
- Modelling and verifying algorithms in Coq
- Interactive Computer Theorem Proving
- Formalization of Mathematics
- Semantic of Proofs and Certified Mathematics
- Iris: Higher-Order Concurrent Separation Logic Lecture Notes
- Formal Reasoning About Programs Adam Chlipala
- Coq Preparation and Boot Camp Types, Logic, and Verification
[编辑] 文档
[编辑] 图书
- 《Software Foundations》 软件基础系列是对可靠软件的数学基础的广泛介绍。该系列的主要创新之处在于,每一个细节都是百分之百的形式化和机器检查:每一卷的整个文本,包括练习,实际上是Coq证明助手的 "证明脚本"。
- 《软件基础》系列广泛地介绍了可靠软件的数学基础,这是《Software Foundations》中文版。
- 《Certified Programming with Dependent Types》
- 《交互式定理证明与程序开发 Coq 归纳构造演算的艺术》
- Mathematical Components
- Modeling and Proving in Computational Type Theory
- Hydras & Co.
- 《Homotopy Type Theory: Univalent Foundations of Mathematics》 The Univalent Foundations Program
[编辑] 案例
- Trusted Logic 经过三年努力,成功地完成 JavaCard 语言的整个执行环境的形式化模拟。这项安全方面的工作获得 EAL7 证书奖(公共标准下最高级别的奖励)。这一形式开发工作使用了 121000 行 Coq 代码,总共 278 个模块。
[编辑] 图集
[编辑] 链接
分享您的观点