The Coq Proof Assistant : Reference Manual : Version 7.2
Abstract
Coq is a proof assistant based on a higher-order logic. Coq allows to handle calculus mathematical assertions and to check mechanically proofs of these assertions. It helps to find formal proofs, and allows extraction of a certified program from the constructive proof of its formal specification. This document is the reference manual for the version V7.2 of Coq which is available from http://coq.inria.fr.
Domains
Other [cs.OH]
Loading...