The development of Coq was initiated by Gérard Huet and Thierry Coquand, and more than 40 people, mainly researchers, have contributed features to the core system since its inception. In the 1990s, ENS Lyon was also part of the project. The development of Coq has been supported since 1984 by INRIA, now in collaboration with École Polytechnique, University of Paris-Sud, Paris Diderot University, and CNRS. When viewed as a programming language, Coq implements a dependently typed functional programming language when viewed as a logical system, it implements a higher-order type theory. 2.1 Four color theorem and SSReflect extension.
#Coq tutorial software
The Association for Computing Machinery awarded Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, and Pierre Castéran with the 2013 ACM Software System Award for Coq.Ĭoq is a wordplay on the name of Thierry Coquand, Calculus of Constructions or "CoC" and is following the French tradition to name tools after animals ( coq in French meaning rooster). Coq is not an automated theorem prover but includes automatic theorem proving tactics ( procedures) and various decision procedures. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification.
An interactive proof session in CoqIDE, showing the proof script on the left and the proof state on the right.Ĭoq is an interactive theorem prover first released in 1989.
0 kommentar(er)
