Category:Coq
From Rosetta Code
Programming Language
Coq is a programming language. It may be used to instruct computers to accomplish a variety of tasks which may or may not be domain-specific.
Listed below are all of the tasks on Rosetta Code which have been solved using Coq.
See also: Coq on the HOPL
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 theorem prover but includes automatic theorem proving tactics and various decision procedures.
