Coq (software)
| Coq
|
|
|---|---|
|
|
|
|
| Basic data
|
|
| developer | TypiCal |
| Publishing year | 1984 |
| Current version |
8.12.0 ( July 27, 2020 ) |
| operating system | Platform independent |
| programming language | Objective CAML , C. |
| category | Machine-Aided Proof |
| License | LGPL ( Free Software ) |
| coq.inria.fr | |
Coq is free software for machine-aided proof of mathematical statements.
Overview
In Coq, data type definitions and executable program parts as well as mathematical statements and proofs are formulated . The statements made usually relate to the defined functions. Coq checks the formal correctness of evidence with the help of its type checker, which is also used otherwise.
Coq also supports the search for evidence and allows, for example, an ML program to be extracted from a formal program specification, including implementation and proof of correctness . Type information that cannot be translated is ignored here. Target code can also be generated from (necessarily constructive) proofs of existence statements.
Coq uses the inductive construction calculus , a form of construction calculus . Coq is not a fully automated evidence system, but does have some evidence tactics and decision-making procedures.
development
Coq is being developed in France as part of the TypiCal (formerly LogiCal) project, a joint project between INRIA , École polytechnique , University of Paris-South and CNRS . Another working group existed at the ENS Lyon . Benjamin Werner is the team leader .
Coq is developed in Objective CAML , a (essentially) functional programming language .
In 2013, Coq received the Programming Languages Software Award from ACM SIGPLAN.
Surname
The French word Coq means rooster or cock and is part of the French tradition of naming scientific development tools after animals. It is also reminiscent of Thierry Coquand , who developed the design calculation together with Gérard Huet .
Four color set
Georges Gonthier (from Microsoft Research , in Cambridge , England ) and Benjamin Werner (from INRIA), with the help of Coq, produced a manageable proof of the four-color theorem , which was completed in 2005.
As a side result of this work, an extension for Coq called ssreflect (" small scale reflection ") was created. Despite the name, most of the features of the extension are general purpose, not just for reflexive evidence. The current version ssreflect 1.2 is free software ( CeCILL license ) and compatible with Coq 8.2.
Feit-Thompson theorem
The set of Feit-Thompson states that every finite group of odd order is solvable. It was proven in 1963 by Walter Feit and John Griggs Thompson .
Georges Gonthier and colleagues succeeded in verifying the evidence with Coq after six years of work in 2012.
literature
- Yves Bertot, Pierre Castéran: Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions , Springer 2004, ISBN 3-540-20854-2
- Adam Chlipala: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant , MIT Press 2013, ISBN 978-0262026659 , available online via Certified Programming with Dependent Types
- Ilya Sergey: Programs and Proofs: Mechanizing Mathematics with Dependent Types , Lecture notes with exercises, URL ilyasergey.net
- Benjamin C. Pierce et al .: Software Foundations , 4 volumes: Volume 1 Logical Foundations , Volume 2 Programming Language Foundations , Volume 3 Verified Functional Algorithms and Volume 4 QuickChick: Property-Based Testing in Coq , URL Software Foundations
Web links
Individual evidence
- ↑ Release 8.12.0 . July 27, 2020 (accessed July 28, 2020).
- ^ The Coq proof assistant Open Source Project on Open Hub: Languages Page . In: Open Hub . (accessed on July 18, 2018).
- ↑ Coq Reference Manual - Calculus of Inductive Constructions ( Memento of December 27, 2012 in the Internet Archive )
- ↑ Gonthier: Formal Proof - the Four-Color Theorem , Notices AMS 2008 (PDF; 2.7 MB)
- ↑ The SSReflect proof language
- ↑ Announcing Ssreflect version 1.2
- ^ Feit-Thompson proved in Coq , Microsoft Research-Inria, September 20, 2012, Web Archive