Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

Cited literature [109 references]  Display  Hide  Download

https://hal.inria.fr/inria-00069919
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 6:34:22 PM
Last modification on : Wednesday, September 16, 2020 - 4:57:01 PM
Long-term archiving on: : Saturday, April 3, 2010 - 10:37:32 PM

Identifiers

  • HAL Id : inria-00069919, version 1

Collections

Citation

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

Share

Metrics

Record views

321

Files downloads

951