Coq
Encyclopedia
In computer science
, Coq is an interactive theorem prover
. It allows the expression of mathematical
assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof
of its formal specification. Coq works within the theory of the calculus of inductive constructions
, a derivative of the calculus of constructions
. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures.
Coq implements a dependently typed functional programming language.
It is developed in France
, in the TypiCal (ex-LogiCal) project, jointly operated by INRIA, École Polytechnique
, Paris-Sud 11 University
and CNRS. There was also formerly a group at École Normale Supérieure de Lyon
. The team leader is Senior Scientist Benjamin Werner. Coq is implemented in Objective Caml
.
The word coq means "cock
" (rooster) in French
, and stems from a tradition of naming French research development tools with animal names. It is also a reference to Thierry Coquand
, who developed the aforementioned calculus of constructions along with Gérard Huet
. Also, at first it was simply called Coc, the acronym of calculus of construction.
, in Cambridge
, England
) and Benjamin Werner (of INRIA) used Coq to create a surveyable proof of the four color theorem
, which was completed in September 2004.
Based on this work, a significant extension to Coq was developed called Ssreflect (which stands for "small scale reflection"). Despite the name, most of the new features added to Coq by Ssreflect are general purpose features, useful not merely for the computational reflection style of proof. These include:
Ssreflect 1.2 is freely available under the open source CeCill-B or Cecill-2.0 license (your choice), and is compatible with Coq 8.2pl1.
Textbooks
Tutorials
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, Coq is an interactive theorem prover
Interactive theorem proving
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by man-machine collaboration...
. It allows the expression of mathematical
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof
Constructive proof
In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object with certain properties by creating or providing a method for creating such an object...
of its formal specification. Coq works within the theory of the calculus of inductive constructions
Calculus of inductive constructions
The calculus of inductive constructions is the underlying core language of the Coq Proof Assistant. It is based on the calculus of constructions extended by inductive definitions as they are known from intuitionistic type theory....
, a derivative of the calculus of constructions
Calculus of constructions
The calculus of constructions is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.-General traits:The CoC is a...
. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures.
Coq implements a dependently typed functional programming language.
It is developed in France
France
The French Republic , The French Republic , The French Republic , (commonly known as France , is a unitary semi-presidential republic in Western Europe with several overseas territories and islands located on other continents and in the Indian, Pacific, and Atlantic oceans. Metropolitan France...
, in the TypiCal (ex-LogiCal) project, jointly operated by INRIA, École Polytechnique
École Polytechnique
The École Polytechnique is a state-run institution of higher education and research in Palaiseau, Essonne, France, near Paris. Polytechnique is renowned for its four year undergraduate/graduate Master's program...
, Paris-Sud 11 University
Paris-Sud 11 University
University of Paris-Sud or University of Paris-Sud or University of Paris XI is a French university distributed among several campuses in the southern suburb of Paris...
and CNRS. There was also formerly a group at École Normale Supérieure de Lyon
École Normale Supérieure de Lyon
The École Normale Supérieure de Lyon is a highly selective grande école located in Lyon, France. As one of France's three Écoles normales supérieures, ENS Lyon is associated with a strong French tradition of excellence and public service...
. The team leader is Senior Scientist Benjamin Werner. Coq is implemented in Objective Caml
Objective Caml
OCaml , originally known as Objective Caml, is the main implementation of the Caml programming language, created by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy and others in 1996...
.
The word coq means "cock
Rooster
A rooster, also known as a cockerel, cock or chanticleer, is a male chicken with the female being called a hen. Immature male chickens of less than a year's age are called cockerels...
" (rooster) in French
French language
French is a Romance language spoken as a first language in France, the Romandy region in Switzerland, Wallonia and Brussels in Belgium, Monaco, the regions of Quebec and Acadia in Canada, and by various communities elsewhere. Second-language speakers of French are distributed throughout many parts...
, and stems from a tradition of naming French research development tools with animal names. It is also a reference to Thierry Coquand
Thierry Coquand
Thierry Coquand is a professor in computer science at the University of Gothenburg, Sweden. He is known for his work in constructive mathematics, especially the calculus of constructions. He received his Ph.D. under the supervision of Gérard Huet.- External links :*...
, who developed the aforementioned calculus of constructions along with Gérard Huet
Gérard Huet
Gérard Pierre Huet is a French computer scientist.- Biography :Gérard Huet graduated from the Université Denis Diderot , Case Western Reserve University, and the Université de Paris....
. Also, at first it was simply called Coc, the acronym of calculus of construction.
Four color theorem and ssreflect extension
Georges Gonthier (of Microsoft ResearchMicrosoft Research
Microsoft Research is the research division of Microsoft created in 1991 for developing various computer science ideas and integrating them into Microsoft products. It currently employs Turing Award winners C.A.R. Hoare, Butler Lampson, and Charles P...
, in Cambridge
Cambridge
The city of Cambridge is a university town and the administrative centre of the county of Cambridgeshire, England. It lies in East Anglia about north of London. Cambridge is at the heart of the high-technology centre known as Silicon Fen – a play on Silicon Valley and the fens surrounding the...
, England
England
England is a country that is part of the United Kingdom. It shares land borders with Scotland to the north and Wales to the west; the Irish Sea is to the north west, the Celtic Sea to the south west, with the North Sea to the east and the English Channel to the south separating it from continental...
) and Benjamin Werner (of INRIA) used Coq to create a surveyable proof of the four color theorem
Four color theorem
In mathematics, the four color theorem, or the four color map theorem states that, given any separation of a plane into contiguous regions, producing a figure called a map, no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color...
, which was completed in September 2004.
Based on this work, a significant extension to Coq was developed called Ssreflect (which stands for "small scale reflection"). Despite the name, most of the new features added to Coq by Ssreflect are general purpose features, useful not merely for the computational reflection style of proof. These include:
- Additional convenient notations for irrefutable and refutable pattern matching, on inductive types with one or two constructors
- Implicit arguments for functions applied to zero arguments - which is useful when programming with higher-order functions
- Concise anonymous arguments
- An improved
settactic with more powerful matching - Support for reflection
Ssreflect 1.2 is freely available under the open source CeCill-B or Cecill-2.0 license (your choice), and is compatible with Coq 8.2pl1.
See also
- Curry-Howard
- Intuitionistic type theoryIntuitionistic type theoryIntuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
- CompcertCompcertCompCert is a formally verified optimizing compiler for a subset of the C programming language which currently targets PowerPC, ARM and 32-bit x86 architectures. This project, led by Xavier Leroy, started officially in 2005, funded by the French institutes ANR and INRIA. The compiler is...
an optimizing compiler for C (programming language)C (programming language)C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
which is fully programmed and proved in Coq.
External links
- The Coq proof assistant - the official English website
- Cocorico!, the Coq Wiki
- MSR Inria math components - hosts the Ssreflect extension
- Constructive Coq Repository at Nijmegen
- Math Classes
Textbooks
- The Coq'Art - A book on Coq by Yves Bertot and Pierre Castéran
- Certified Programming with Dependent Types - online draft textbook by Adam Chlipala
- Software Foundations - Online textbook by Benjamin C. PierceBenjamin C. PierceBenjamin Crawford Pierce is an American professor of computer science at the University of Pennsylvania. Pierce joined Penn in 1998 from Indiana University and held research positions at the University of Cambridge and the University of Edinburgh. He received his Ph.D. from Carnegie Mellon...
et al.
Tutorials
- Introduction to the Coq Proof Assistant Video lecture by Andrew AppelAndrew AppelAndrew Wilson Appel is the Eugene Higgins Professor of computer science at Princeton University, New Jersey. He is especially well-known because of his compiler books, the Modern Compiler Implementation in ML series, as well as Compiling With Continuations...
at Institute for Advanced StudyInstitute for Advanced StudyThe Institute for Advanced Study, located in Princeton, New Jersey, United States, is an independent postgraduate center for theoretical research and intellectual inquiry. It was founded in 1930 by Abraham Flexner... - Video tutorials for the Coq proof assistant by Andrej Bauer.