Skip to Main content Skip to Navigation
Other publications

The Coq Proof Assistant, version 8.7.1

The Coq Development Team 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19
1 PI.R2 - Design, study and implementation of languages for proofs and programs
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
2 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
3 ASCOLA - Aspect and Composition Languages
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
6 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
Abstract : Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.
Document type :
Other publications
Complete list of metadatas

https://hal.inria.fr/hal-01673716
Contributor : Matthieu Sozeau <>
Submitted on : Sunday, December 31, 2017 - 3:04:33 PM
Last modification on : Tuesday, August 4, 2020 - 8:21:06 AM

Identifiers

Citation

The Coq Development Team. The Coq Proof Assistant, version 8.7.1. 2017, pp.1-571. ⟨10.5281/zenodo.1133970⟩. ⟨hal-01673716⟩

Share

Metrics

Record views

298