Credits
Coq is a proof assistant for higher-order logic, allowing the
development of computer programs consistent with their formal
specification. It is the result of about ten years of research of the
Coq project. We shall briefly survey here three main aspects: the
logical language in which we write our axiomatizations and
specifications, the proof assistant which allows the development
of verified mathematical proofs, and the program extractor which
synthesizes computer programs obeying their formal specifications,
written as logical assertions in the language.
The logical language used by Coq is a variety of type theory,
called the Calculus of Inductive Constructions. Without going
back to Leibniz and Boole, we can date the creation of what is now
called mathematical logic to the work of Frege and Peano at the turn
of the century. The discovery of antinomies in the free use of
predicates or comprehension principles prompted Russell to restrict
predicate calculus with a stratification of types. This effort
culminated with Principia Mathematica, the first systematic
attempt at a formal foundation of mathematics. A simplification of
this system along the lines of simply typed lambda-calculus
occurred with Church's Simple Theory of Types. The
lambda-calculus notation, originally used for expressing
functionality, could also be used as an encoding of natural deduction
proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the
Automath project, the first full-scale attempt to develop and
mechanically verify mathematical proofs. This effort culminated with
Jutting's verification of Landau's Grundlagen in the 1970's.
Exploiting this Curry-Howard isomorphism, notable achievements in
proof theory saw the emergence of two type-theoretic frameworks; the
first one, Martin-Löf's Intuitionistic Theory of Types,
attempts a new foundation of mathematics on constructive principles.
The second one, Girard's polymorphic lambda-calculus Fomega, is
a very strong functional system in which we may represent higher-order
logic proof structures. Combining both systems in a higher-order
extension of the Automath languages, T. Coquand presented in 1985 the
first version of the Calculus of Constructions, CoC. This strong
logical system allowed powerful axiomatizations, but direct inductive
definitions were not possible, and inductive notions had to be defined
indirectly through functional encodings, which introduced
inefficiencies and awkwardness. The formalism was extended in 1989 by
T. Coquand and C. Paulin with primitive inductive definitions, leading
to the current Calculus of Inductive Constructions. This
extended formalism is not rigorously defined here. Rather, numerous
concrete examples are discussed. We refer the interested reader to
relevant research papers for more information about the formalism, its
meta-theoretic properties, and semantics. However, it should not be
necessary to understand this theoretical material in order to write
specifications. It is possible to understand the Calculus of Inductive
Constructions at a higher level, as a mixture of predicate calculus,
inductive predicate definitions presented as typed PROLOG, and
recursive function definitions close to the language ML.
Automated theorem-proving was pioneered in the 1960's by Davis and
Putnam in propositional calculus. A complete mechanization (in the
sense of a semi-decision procedure) of classical first-order logic was
proposed in 1965 by J.A. Robinson, with a single uniform inference
rule called resolution. Resolution relies on solving equations
in free algebras (i.e. term structures), using the unification
algorithm. Many refinements of resolution were studied in the
1970's, but few convincing implementations were realized, except of
course that PROLOG is in some sense issued from this effort. A less
ambitious approach to proof development is computer-aided
proof-checking. The most notable proof-checkers developed in the
1970's were LCF, designed by R. Milner and his colleagues at U.
Edinburgh, specialized in proving properties about denotational
semantics recursion equations, and the Boyer and Moore theorem-prover,
an automation of primitive recursion over inductive data types. While
the Boyer-Moore theorem-prover attempted to synthesize proofs by a
combination of automated methods, LCF constructed its proofs through
the programming of tactics, written in a high-level functional
meta-language, ML.
The salient feature which clearly distinguishes our proof assistant
from say LCF or Boyer and Moore's, is its possibility to extract
programs from the constructive contents of proofs. This computational
interpretation of proof objects, in the tradition of Bishop's
constructive mathematics, is based on a realizability interpretation,
in the sense of Kleene, due to C. Paulin. The user must just mark his
intention by separating in the logical statements the assertions
stating the existence of a computational object from the logical
assertions which specify its properties, but which may be considered
as just comments in the corresponding program. Given this information,
the system automatically extracts a functional term from a consistency
proof of its specifications. This functional term may be in turn
compiled into an actual computer program. This methodology of
extracting programs from proofs is a revolutionary paradigm for
software engineering. Program synthesis has long been a theme of
research in artificial intelligence, pioneered by R. Waldinger. The
Tablog system of Z. Manna and R. Waldinger allows the deductive
synthesis of functional programs from proofs in tableau form of their
specifications, written in a variety of first-order logic. Development
of a systematic programming logic, based on extensions of
Martin-Löf's type theory, was undertaken at Cornell U. by the Nuprl
team, headed by R. Constable. The first actual program extractor, PX,
was designed and implemented around 1985 by S. Hayashi from Kyoto
University. It allows the extraction of a LISP program from a proof
in a logical system inspired by the logical formalisms of S. Feferman.
Interest in this methodology is growing in the theoretical computer
science community. We can foresee the day when actual computer systems
used in applications will contain certified modules, automatically
generated from a consistency proof of their formal specifications. We
are however still far from being able to use this methodology in a
smooth interaction with the standard tools from software engineering,
i.e. compilers, linkers, run-time systems taking advantage of special
hardware, debuggers, and the like. We hope that Coq can be of use
to researchers interested in experimenting with this new methodology.
A first implementation of CoC was started in 1984 by G. Huet and T.
Coquand. Its implementation language was CAML, a functional
programming language from the ML family designed at INRIA in
Rocquencourt. The core of this system was a proof-checker for CoC seen
as a typed lambda-calculus, called the Constructive Engine.
This engine was operated through a high-level notation permitting the
declaration of axioms and parameters, the definition of mathematical
types and objects, and the explicit construction of proof objects
encoded as lambda-terms. A section mechanism, designed and
implemented by G. Dowek, allowed hierarchical developments of
mathematical theories. This high-level language was called the
Mathematical Vernacular. Furthermore, an interactive
Theorem Prover permitted the incremental construction of proof
trees in a top-down manner, subgoaling recursively and backtracking
from dead-alleys. The theorem prover executed tactics written in CAML,
in the LCF fashion. A basic set of tactics was predefined, which the
user could extend by his own specific tactics. This system (Version
4.10) was released in 1989. Then, the system was extended to deal
with the new calculus with inductive types by C. Paulin, with
corresponding new tactics for proofs by induction. A new standard set
of tactics was streamlined, and the vernacular extended for tactics
execution. A package to compile programs extracted from proofs to
actual computer programs in CAML or some other functional language was
designed and implemented by B. Werner. A new user-interface, relying
on a CAML-X interface by D. de Rauglaudre, was designed and
implemented by A. Felty. It allowed operation of the theorem-prover
through the manipulation of windows, menus, mouse-sensitive buttons,
and other widgets. This system (Version 5.6) was released in 1991.
Coq was ported to the new implementation Caml-light of X. Leroy and
D. Doligez by D. de Rauglaudre (Version 5.7) in 1992. A new version
of Coq was then coordinated by C. Murthy, with new tools designed
by C. Parent to prove properties of ML programs (this methodology is
dual to program extraction) and a new user-interaction loop. This
system (Version 5.8) was released in May 1993. A Centaur interface
CTCoq was then developed by Y. Bertot from the Croap project
from INRIA-Sophia-Antipolis.
In parallel, G. Dowek and H. Herbelin developed a new proof engine,
allowing the general manipulation of existential variables
consistently with dependent types in an experimental version of Coq
(V5.9).
The version V5.10 of Coq is based on a generic system for
manipulating terms with binding operators due to Chet Murthy. A new
proof engine allows the parallel development of partial proofs for
independent subgoals. The structure of these proof trees is a mixed
representation of derivation trees for the Calculus of Inductive
Constructions with abstract syntax trees for the tactics scripts,
allowing the navigation in a proof at various levels of details. The
proof engine allows generic environment items managed in an
object-oriented way. This new architecture, due to C. Murthy,
supports several new facilities which make the system easier to extend
and to scale up:
-
User-programmable tactics are allowed
- It is possible to separately verify development modules, and to
load their compiled images without verifying them again - a quick
relocation process allows their fast loading
- A generic parsing scheme allows user-definable notations, with a
symmetric table-driven pretty-printer
- Syntactic definitions allow convenient abbreviations
- A limited facility of meta-variables allows the automatic
synthesis of certain type expressions, allowing generic notations
for e.g. equality, pairing, and existential quantification.
In the Fall of 1994, C. Paulin-Mohring replaced the structure of
inductively defined types and families by a new structure, allowing
the mutually recursive definitions. P. Manoury implemented a
translation of recursive definitions into the primitive recursive
style imposed by the internal recursion operators, in the style of the
ProPre system. C. Muñoz implemented a decision procedure for
intuitionistic propositional logic, based on results of R. Dyckhoff.
J.C. Filliâtre implemented a decision procedure for first-order
logic without contraction, based on results of J. Ketonen and R.
Weyhrauch. Finally C. Murthy implemented a library of inversion
tactics, relieving the user from tedious definitions of ``inversion
predicates''.
Rocquencourt, Feb. 1st 1995
Gérard Huet
Credits: addendum for version 6.1
The present version 6.1 of Coq is based on the V5.10 architecture. It
was ported to the new language Objective Caml by Bruno Barras. The
underlying framework has slightly changed and allows more conversions
between sorts.
The new version provides powerful tools for easier developments.
Cristina Cornes designed an extension of the Coq syntax to allow
definition of terms using a powerful pattern-matching analysis in the
style of ML programs.
Amokrane Saïbi wrote a mechanism to simulate
inheritance between types families extending a proposal by Peter
Aczel. He also developed a mechanism to automatically compute which
arguments of a constant may be inferred by the system and consequently
do not need to be explicitly written.
Yann Coscoy designed a command which explains a proof term using
natural language. Pierre Crégut built a new tactic which solves
problems in quantifier-free Presburger Arithmetic. Both
functionalities have been integrated to the Coq system by Hugo
Herbelin.
Samuel Boutin designed a tactic for simplification of commutative
rings using a canonical set of rewriting rules and equality modulo
associativity and commutativity.
Finally the organisation of the Coq distribution has been supervised
by Jean-Christophe Filliâtre with the help of Judicaël Courant
and Bruno Barras.
Lyon, Nov. 18th 1996
Christine Paulin
Credits: addendum for version 6.2
In version 6.2 of Coq, the parsing is done using camlp4, a
preprocessor and pretty-printer for CAML designed by Daniel de
Rauglaudre at INRIA. Daniel de Rauglaudre made the first adaptation
of Coq for camlp4, this work was continued by Bruno Barras who also
changed the structure of Coq abstract syntax trees and the primitives
to manipulate them. The result of
these changes is a faster parsing procedure with greatly improved
syntax-error messages. The user-interface to introduce grammar or
pretty-printing rules has also changed.
Eduardo Giménez redesigned the internal
tactic libraries, giving uniform names
to Caml functions corresponding to Coq tactic names.
Bruno Barras wrote new more efficient reductions functions.
Hugo Herbelin introduced more uniform notations in the Coq
specification language: the definitions by fixpoints and
pattern-matching have a more readable syntax. Patrick Loiseleur
introduced user-friendly notations for arithmetic expressions.
New tactics were introduced: Eduardo Giménez improved a mechanism to
introduce macros for tactics, and designed special tactics for
(co)inductive definitions; Patrick Loiseleur designed a tactic to
simplify polynomial expressions in an arbitrary commutative ring which
generalizes the previous tactic implemented by Samuel Boutin.
Jean-Christophe Filliâtre introduced a tactic for refining a goal,
using a proof term with holes as a proof scheme.
David Delahaye designed the SearchIsos tool to search an
object in the library given its type (up to isomorphism).
Henri Laulhère produced the Coq distribution for the Windows environment.
Finally, Hugo Herbelin was the main coordinator of the Coq
documentation with principal contributions by Bruno Barras, David Delahaye,
Jean-Christophe Filliâtre, Eduardo
Giménez, Hugo Herbelin and Patrick Loiseleur.
Orsay, May 4th 1998
Christine Paulin
Credits: addendum for version 6.3
The main changes in version V6.3 was the introduction of a few new tactics
and the extension of the guard condition for fixpoint definitions.
B. Barras extended the unification algorithm to complete partial terms
and solved various tricky bugs related to universes.
D. Delahaye developed the AutoRewrite tactic. He also designed the new
behavior of Intro and provided the tacticals First and
Solve.
J.-C. Filliâtre developed the Correctness tactic.
E. Giménez extended the guard condition in fixpoints.
H. Herbelin designed the new syntax for definitions and extended the
Induction tactic.
P. Loiseleur developed the Quote tactic and
the new design of the Auto
tactic, he also introduced the index of
errors in the documentation.
C. Paulin wrote the Focus command and introduced
the reduction functions in definitions, this last feature
was proposed by J.-F. Monin from CNET Lannion.
Orsay, Dec. 1999
Christine Paulin
Credits: versions 7
The version V7 is a new implementation started in September 1999 by
Jean-Christophe Filliâtre. This is a major revision with respect to
the internal architecture of the system. The Coq version 7.0 was
distributed in March 2001, version 7.1 in September 2001, version
7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in
February 2003.
Jean-Christophe Filliâtre designed the architecture of the new system, he
introduced a new representation for environments and wrote a new kernel
for type-checking terms. His approach was to use functional
data-structures in order to get more sharing, to prepare the addition
of modules and also to get closer to a certified kernel.
Hugo Herbelin introduced a new structure of terms with local
definitions. He introduced ``qualified'' names, wrote a new
pattern-matching compilation algorithm and designed a more compact
algorithm for checking the logical consistency of universes. He
contributed to the simplification of Coq internal structures and the
optimisation of the system. He added basic tactics for forward
reasoning and coercions in patterns.
David Delahaye introduced a new language for tactics. General tactics
using pattern-matching on goals and context can directly be written
from the Coq toplevel. He also provided primitives for the design
of user-defined tactics in Caml.
Micaela Mayero contributed the library on real numbers.
Olivier Desmettre extended this library with axiomatic
trigonometric functions, square, square roots, finite sums, Chasles
property and basic plane geometry.
Jean-Christophe Filliâtre and Pierre Letouzey redesigned a new
extraction procedure from Coq terms to Caml or
Haskell programs. This new
extraction procedure, unlike the one implemented in previous version
of Coq is able to handle all terms in the Calculus of Inductive
Constructions, even involving universes and strong elimination. P.
Letouzey adapted user contributions to extract ML programs when it was
sensible.
Jean-Christophe Filliâtre wrote coqdoc, a documentation
tool for Coq libraries usable from version 7.2.
Bruno Barras improved the reduction algorithms efficiency and
the confidence level in the correctness of Coq critical type-checking
algorithm.
Yves Bertot designed the SearchPattern and
SearchRewrite tools and the support for the pcoq interface
(http://www-sop.inria.fr/lemme/pcoq/).
Micaela Mayero and David Delahaye introduced Field, a decision tactic for commutative fields.
Christine Paulin changed the elimination rules for empty and singleton
propositional inductive types.
Loïc Pottier developed Fourier, a tactic solving linear inequalities on real numbers.
Pierre Crégut developed a new version based on reflexion of the Omega
decision tactic.
Claudio Sacerdoti Coen designed an XML output for the Coq
modules to be used in the Hypertextual Electronic Library of
Mathematics (HELM cf http://www.cs.unibo.it/helm).
A library for efficient representation of finite maps using binary trees
contributed by Jean Goubault was integrated in the basic theories.
Jacek Chrzaszcz designed and implemented the module system of
Coq whose foundations are in Judicaël Courant's PhD thesis.
The development was coordinated by C. Paulin.
Many discussions within the Démons team and the LogiCal project
influenced significantly the design of Coq especially with
J. Courant, P. Courtieu, J. Duprat, J. Goubault, A. Miquel,
C. Marché, B. Monate and B. Werner.
Intensive users suggested improvements of the system :
Y. Bertot, L. Pottier, L. Théry , P. Zimmerman from INRIA,
C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R & D.
Orsay, May. 2002
Hugo Herbelin & Christine Paulin
Credits: version 8.0
Coq version 8 is a major revision of the Coq proof assistant.
First, the underlying logic is slightly different. The so-called impredicativity of the sort Set has been dropped. The main
reason is that it is inconsistent with the principle of description
which is quite a useful principle for formalizing mathematics within classical logic. Moreover, even in an constructive
setting, the impredicativity of Set does not add so much in
practice and is even subject of criticism from a large part of the
intuitionistic mathematician community. Nevertheless, the
impredicativity of Set remains optional for users interested in
investigating mathematical developments which rely on it.
Secondly, the concrete syntax of terms has been completely
revised. The main motivations were
-
a more uniform, purified style: all constructions are now lowercase,
with a functional programming perfume (e.g. abstraction is now
written fun), and more directly accessible to the novice
(e.g. dependent product is now written forall and allows
omission of types). Also, parentheses and are no longer mandatory
for function application.
- extensibility: some standard notations (e.g. ``<'' and ``>'') were
incompatible with the previous syntax. Now all standard arithmetic
notations (=, +, *, /, <, <=, ... and more) are directly part of the
syntax.
Together with the revision of the concrete syntax, a new mechanism of
interpretation scopes permits to reuse the same symbols
(typically +, -, *, /, <, <=) in various mathematical theories without
any ambiguities for Coq, leading to a largely improved readability of
Coq scripts. New commands to easily add new symbols are also
provided.
Coming with the new syntax of terms, a slight reform of the tactic
language and of the language of commands has been carried out. The
purpose here is a better uniformity making the tactics and commands
easier to use and to remember.
Thirdly, a restructuration and uniformisation of the standard library
of Coq has been performed. There is now just one Leibniz' equality
usable for all the different kinds of Coq objects. Also, the set of
real numbers now lies at the same level as the sets of natural and
integer numbers. Finally, the names of the standard properties of
numbers now follow a standard pattern and the symbolic
notations for the standard definitions as well.
The fourth point is the release of CoqIDE, a new graphical
gtk2-based interface fully integrated to Coq. Close in style from
the Proof General Emacs interface, it is faster and its integration
with Coq makes interactive developments more friendly. All
mathematical Unicode symbols are usable within CoqIDE.
Finally, the module system of Coq completes the picture of Coq
version 8.0. Though released with an experimental status in the previous
version 7.4, it should be considered as a salient feature of the new
version.
Besides, Coq comes with its load of novelties and improvements: new
or improved tactics (including a new tactic for solving first-order
statements), new management commands, extended libraries.
Bruno Barras and Hugo Herbelin have been the main contributors of the
reflexion and the implementation of the new syntax. The smart
automatic translator from old to new syntax released with Coq is also
their work with contributions by Olivier Desmettre.
Hugo Herbelin is the main designer and implementor of the notion of
interpretation scopes and of the commands for easily adding new notations.
Hugo Herbelin is the main implementor of the restructuration of the
standard library.
Pierre Corbineau is the main designer and implementor of the new
tactic for solving first-order statements in presence of inductive
types. He is also the maintainer of the non-domain specific automation
tactics.
Benjamin Monate is the developer of the CoqIDE graphical
interface with contributions by Jean-Christophe Filliâtre, Pierre
Letouzey and Claude Marché.
Claude Marché coordinated the edition of the Reference Manual for
Coq V8.0.
Pierre Letouzey and Jacek Chrzaszcz respectively maintained the
extraction tool and module system of Coq.
Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and
contributors from Sophia-Antipolis and Nijmegen participated to the
extension of the library.
Hugo Herbelin and Christine Paulin coordinated the development which
was under the responsability of Christine Paulin.
Palaiseau & Orsay, Apr. 2004
Hugo Herbelin & Christine Paulin