- In dec 96 the Coq system version V6.1 was released. It is joint work by the ENS Lyon and INRIA Rocquencourt Sites. The main improvements with respect to the previous versions were :
- the efficiency (approximately 5 times faster) due to the choice of a new implementation language : objective Caml
- the integration of a fast package for arithmetic computation based on binary arithmetic and the integration of a decision procedure for a fragment of Presburger Arithmetic ddeveloped by P. Crégut (from CNET, the research center of French Telecommunications)
- the integration of a package for defining terms by pattern-matching (Cristina Cornes-Rocquencourt)
- the integration of a package for implicit coercions (Amokrane Saïbi-Rocquencourt)
Work in Lyon was principally concerned with:- meta-theory of inductive and coinductive definitions (Eduardo Giménez, Christine Paulin)
- the design of a module language on top of PTS (Judicaël Courant)
- automatic detection of dead code and other code analysis using typing (Frédéric Prost interacted with Ferruccio Damiani from Torino, they wrote a common paper to appear in TYPES'96)
- proofs of imperative programs : Jean-Christophe Filliâtre designed a translation of imperative program into functional program. The usual realisability interpretation of programs as witness for proofs applied to the translated program generates proofs obligation analogous to the one given by a direct proof with Hoare Logic.
- proof development :
* a proof of an algorithm for synchronisation in cellular automata (firing squad) using 6 states and in minimal time was developed by Jean Duprat.
* a formalisation of IEEE 754 norm for arithmetic was developed by Patrick Loiseleur
* Jean-Christophe Filliatre developed a proof of Kleene theorem for finite automata (equivalence between regular expressions and languages recognised by finite automata) a program that compute the automata from the regular expression was extracted.
Cristina Cornes has defended her thesis in which she proposes an unification
algorithm for the Calculus of inductive constructions and applications to the
compilation of recursively defined functions.
César Muñoz has defended his thesis in which he proposes an extension of
the Calculus of constructions with explicit substitutions allowing to
process incomplete proofs. Gilles Dowek and Benjamin Werner have started an
implementation of a prototype using this formalism.
Bruno Barras has pursued his work on the formalization of the meta-theory
of type systems in the system Coq towards its bootstrap. He is currently
working on the formalization of inductive types.
Micaela Mayero has developped an axiomatization of real numbers in the system
Coq.
Benjamin Werner and Gilberto Perez Vega have worked on the formalization of
the proof of Buchberger's algorithm.
Eduardo Gimenez has inverstigated the use of co-inductive types to
prove properties of protocols.
David Delahaye has designed a search tool for data bases of theorems.
Amokrane Saïbi has implemented rewrites tactics in the system Coq.
In the line of previous works of Peter Aczel and Thierry Coquand, Benjamin
Werner has developed a encoding of set theory in the Calculus of inductive
constructions and vice-versa. He has proposed a new formulation of the
axiom of choice in type theory that permits to derive the set theoretical
axiom of choice.
Gilles Dowek has defined a notion of cut associated to the axioms of a
first-order presentation of higher-order logic and showed that the
usual cut elimination proof for higher-order logic works for this system.
Gilles Dowek, Thérèse Hardin and Claude Kirchner, have developped a new
proof search method for first-order logic extended with a rewrite system.
Applying this method to a first-order presentation of higher-order logic
permits to retrieve higher-order resolution.
Benjamin Werner and Paul-André Melliès have proposed a new proof
technique for normalization in pure type systems.
Hugo Herbelin and Pierre-Louis Curien has pursued their work on game semantics
for computation.
Gérard Huet and Henri Laulhere have finished a work on the relation
between combinators and infinite Böhm trees.
Industrial use of Coq in France
In France, Coq was used by the G.I.E. Dyade (Bull-INRIA) for developing proofs of cryptographic protocols involved in electronical transactions. Coq is also used by CNET in the validation of algorithms involved in the ATM protocols.
Cooperation between partners
Some references: