Rocq prover
Sign in to savethumb|300x300px|An interactive proof session in CoqIDE, showing the proof script on the left and the proof state on the right.
Key facts
- Software.name
- The Rocq Prover
- Software.logo
- Rocq logo.svg
- Software.author
- Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, Pierre Castéran
- Software.developer
- INRIA, École Polytechnique, University of Paris-Sud, Paris Diderot University, CNRS, ENS Lyon
- Software.released
- (version 4.10)
- Software.operating system
- Cross-platform
- Software.language
- English
- Software.programming language
- OCaml
- Software.genre
- Proof assistant
- Software.license
- LGPLv2.1
via Wikipedia infobox
Article
10 sectionsContents
- Overview
- Notable uses
- Four color theorem and SSReflect extension
- Other applications
- Tactic language
- Name
- Awards
- See also
- References
- External links
thumb|300x300px|An interactive proof session in CoqIDE, showing the proof script on the left and the proof state on the right.
The Rocq Prover (formerly named Coq) is an interactive theorem prover first released in 1989. It allows the expression of mathematical assertions, mechanical checking of proofs of these assertions, assists in finding formal proofs using proof automation routines and extraction of a certified program from the constructive proof of its formal specification.