{{language|Rocq
|site=https://rocq-prover.org/
}}
The '''Rocq Prover''' (previously known as '''Coq''') is a proof assistant application. 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. Rocq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Rocq is not an automated [[wp:Theorem_prover|theorem prover]] but includes automatic theorem proving tactics and various decision procedures.

==Citations==
* [[wp:Rocq|Rocq]]

[[Category:Mathematical programming languages]]