HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

The Coq Proof Assistant : Reference Manual : Version 7.2

The Coq 1
1 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Document type :
Complete list of metadata

Cited literature [109 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 6:34:22 PM
Last modification on : Friday, February 4, 2022 - 3:23:48 AM
Long-term archiving on: : Saturday, April 3, 2010 - 10:37:32 PM


  • HAL Id : inria-00069919, version 1


The Coq. The Coq Proof Assistant : Reference Manual : Version 7.2. RT-0255, INRIA. 2002, pp.290. ⟨inria-00069919⟩



Record views


Files downloads