Category:Coq: Difference between revisions
Content added Content deleted
m (language stub) |
m (fill in something to remove _stub_, for testing purpose) |
||
| Line 1: | Line 1: | ||
{{language|Coq}}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. |
|||
{{language|Coq}}{{stub}} |
|||
==Citations== |
|||
* [[wp:Coq|Coq]] |
|||