9 lines
No EOL
663 B
Text
9 lines
No EOL
663 B
Text
{{language|Coq
|
|
|site=http://coq.inria.fr
|
|
}}
|
|
In computer science, 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. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated [[wp:Theorem_prover|theorem prover]] but includes automatic theorem proving tactics and various decision procedures.
|
|
|
|
==Citations==
|
|
* [[wp:Coq|Coq]]
|
|
|
|
[[Category:Mathematical programming languages]] |