Sites Inria

Version française

Mathilde De Vos -

Chronology: Seven Key Dates

On 23 January 2013 the Coq program is to receive the SIGPLAN Programming Languages Software Award. This prize is conferred on an annual basis in recognition of a software program that has had a significant impact on research and development in the field of programming languages. Here are seven key dates in the project's history.


The research undertaken by Thierry Coquand for his thesis lays the foundations for the "Calculus of Constructions". This theory will lead to the development of proof within the Calculus of Constructions. This is the origin of "CoC".


First public announcement. CoC had until this time been available exclusively to a small number of specialist experimenters.


CoC is re-named "Coq". This change denotes a major modification of the program, i.e. the introduction of a new primitive notion of objects called "inductive types". This universal notion proves itself to be extremely natural in terms of logic and programming. This change also provides primitive principles of recursion and induction, thus making a break with axioms that were not in harmony with the basic principles of the Calculus of Constructions. The new version is thus of a purely calculative nature, and based on a constructive logic. In short, all proofs can be executed as programs.


A new method of implementation constructed around a clearly defined kernel. This kernel checks the logical correction, and verifies the proofs. The smaller it is, the more reliable it is.


Re-working of the syntax outside the kernel, standardisation of libraries. The aim is to enable new advances. This is the start of the process of expansion for Coq, particularly following the publication of Coq'Art, an introductory study written by Yves Bertot and Pierre Castéran .


Coq enables the certification to an absolute degree of the properties of the Java Card code. This means that absolute confidence can be accorded to certain key functions of the Java Card operational system used by a large number of smart cards (credit cards, SIM cards, etc.)


ACM SIGPLAN confers the SIGPLAN Programming Languages Software Award on Coq, thus giving recognition to a project that has lasted for nearly 30 years. The prize will be presented in person in San Diego in January 2014 to a committee consisting of Gérard Huet , Yves Bertot , Jean-Christophe Filliâtre and Matthieu Sozeau .

Keywords: Proof SIGPLAN Programming Languages Software Award ACM SIGPLAN Award Coq