https://en.wikipedia.org/wiki/Coq
"Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures."
"The Association for Computing Machinery rewarded Thierry Coquand, Gérard Pierre Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot and Pierre Castéran with the 2013 ACM Software System Award for Coq."
"The word coq means "rooster" in French, and stems from a local tradition of naming French research development tools with animal names.[4] Up to 1991, Coquand was implementing a language called the Calculus of Constructions and it was simply called CoC at this time. In 1991, a new implementation based on the extended Calculus of Inductive Constructions was started and the name changed from CoC to Coq, also an indirect reference to Thierry Coquand who developed the Calculus of Constructions along with Gérard Pierre Huet and the Calculus of Inductive Constructions along with Christine Paulin-Mohring."https://coq.inria.fr/
"Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching."
Github Resources:
https://github.com/coq
A port of Coq to Javascript
- https://github.com/ejgallego/jscoq
- "JsCoq is written in ES2017"
- "Coq is compiled to JavaScript using the js_of_ocaml compiler."
Tutorial Resources:
- https://softwarefoundations.cis.upenn.edu/current/index.html
- https://softwarefoundations.cis.upenn.edu/current/lf-current/index.html
- https://softwarefoundations.cis.upenn.edu/current/plf-current/index.html
- https://softwarefoundations.cis.upenn.edu/current/vfa-current/index.html
- https://softwarefoundations.cis.upenn.edu/current/qc-current/index.html
- https://arxiv.org/pdf/1803.01466.pdf
- ("Learning how to Prove: From the Coq Proof Assistant to Textbook Style")
- https://www.lri.fr/~paulin/LASER/course-notes.pdf
- ("Introduction to the Coq proof-assistant for practical software verification")
- http://www.cs.umd.edu/~rrand/cufp_2015/
- ("CUFP 2015: An Introduction to the Coq Proof Assistant, By Arthur Azevedo de Amorim and Robert Rand, University of Pennsylvania")
- https://ncatlab.org/nlab/show/Coq
- https://www.youtube.com/watch?v=3WBUHEVr56c
- ("Introduction to the Coq Proof Assistant - Andrew Appel")
Sandboxes:
- https://x80.org/rhino-coq/
- ("JsCoq Interactive Online System")
Note:
My awareness and interest in Coq was spurred by this AI podcast interview that Lex Fridman conducted with George Holtz (re: Comma.ai, OpenPilot, and Autonomous Vehicles)
(Bloomberg: "The First Person to Hack the iPhone Built a Self-Driving Car. In His Garage")
(Bloomberg: "The First Person to Hack the iPhone Built a Self-Driving Car. In His Garage")
No comments:
Post a Comment