software . 2018

The Coq Proof Assistant, version 8.8.0

Team, The Coq Development;
Open Source English
  • Published: 17 Apr 2018
  • Publisher: HAL CCSD
  • Country: 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. Coq version 8.10 contains two major new features: support for a native fixed-precision integer type and a new sort SP...
Subjects
free text keywords: [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], proof assistant, mathematical software, formal proofs
Zenodo
Software . 2018
Provider: Datacite
Zenodo
Software . 2018
Provider: Datacite
Zenodo
Software . 2017
Provider: Datacite
Zenodo
Software . 2017
Provider: Datacite
Any information missing or wrong?Report an Issue