The Coq Proof Assistant - Zero-default Programs in Safety Critical Software
by Christine Paulin
The Coq research team at INRIA elaborates a language and environment for the mechanisation of formal proofs. It develops and distributes the Coq proof assistant. This environment is dedicated to the elaboration and certification of zero-default programs in safety critical software.
Coq was a project common to INRIA Rocquencourt and the Laboratoire de l'Informatique du Parallélisme (URA CNRS 1398) of the École Normale Supérieure de Lyon from January 1994 to September 1997. The Laboratoire de Recherche en Informatique (URA CNRS 410) at the University Paris 11 is now also involved in this project.
The Coq Proof Assistant provides a powerful specification language based on an intuitionistic type theory. In this language, it is possible to write pure functional programs manipulating finite or infinite objects in concrete data types, to describe intentionally a mathematical set by a property satisfied by its elements or to represent an inductive relation by a set of closure properties similar to a Prolog program.
The proofs in Coq are represented by terms. The kernel of Coq is a type-checker for these terms which only accepts well-formed constructions corresponding to meaningful specifications and correct proofs. It is possible to build a proof in a forward direction using proof terms or in a backward direction using tactics in the tradition of the LCF proof environment.
The high-level description language of Coq is well-suited for the development of general abstract theories. During the last few years, Coq has been used for large developments in theoretical computer science: Category Theory (Amokrane Saïbi, INRIA), the representation of pi-calculus (Daniel Hirshkoff, CERMICS), proof of an optimal algorithm for the firing squad problem in Cellular Automata (Jean Duprat, ENS Lyon). We are currently investigating the proof of the Coq type-checker itself (Bruno Barras).
Coq is currently used intensively for the modelisation and verification of cryptographic protocols for electronic transactions by the VIP action in the GIE Dyade (Bull-INRIA, see ERCIM news no 30).
A specificity of Coq with respect to other higher-order proof-checker is the possible interpretation of constructive proofs as executable programs. From a constructive proofs of existence, it is possible to derive an algorithm to compute a witness. A Coq proof automatically generates an ML program which represents the computational meaning of the proof and gives a certified prototype for the given problem. Conversely from a functional program and a specification one can generate proof obligations that are sufficient conditions for the code to be correct. This methodology has been applied to various algorithms (sorting, tautology checker, type-checker,..). It is sometimes possible to reflect an abstract result proved in Coq as a strategy for doing Coq proofs. For instance Samuel Boutin developed an algorithm to decide equality of terms in abstract commutative rings and then reflected this theorem in Coq in order to derive elegant and efficient proofs of equality of arithmetic expressions. This is one step towards the integration of automatic and interactive theorem proving.
Two main issues for a larger impact of the Coq effort on formal proofs development are:
- to keep the specification language both conceptually simple and powerful
- to provide more assistance in the construction of proofs in particular by integrating automatic deduction techniques.
The Coq project participates to an Esprit Working Group "Types " together with Cambridge, Edinburgh, Gothenburg , Helsinki, Manchester, Munich, Nijmegen, Oxford, Paris 7, Torino, Udine and Utrecht.
Please contact:
Christine Paulin-Mohring
Tel: + 33 1 39 63 55 70
E-mail: Christine.Paulin@inria.fr