Next: INRIA Sophia-Antipolis Up: Progress Report Previous: Chalmers

ENS Lyon and INRIA Rocquencourt

Since september 1997, part of the team in Lyon has moved to LRI Université Paris Sud.

1 The Coq Proof Assistant

In july 99, the Coq version V6.3 [1, 8] has been released.

1.1 Automatic tactics

The main novelties concern automatic tactics :

Coq Auto tactic searchs in a database of basic tactics. It has been rewritten by P. Loiseleur. It is now possible to split the tactics into distinct packages that can be invoked independently. The possibility to extend this database with an arbitrary tactic has been added.
A analoguous (still experimental) tactic to perform rewriting using databases of rewrite lemmas and called AutoRewrite has been designed by D. Delahaye.
We continue to investigate the use of reflexion technics for automatic proofs.
- P. Loiseleur designed and implemented a tactic called Quote to "inverse" automatically the interpretation function used for reflexion.
- P. Loiseleur extended the Ring tactic for proving equalities in abelian rings to work with structure in the predicative universe Type (in particular the reals).
- J. Goubault together with K. Verma developed a library for manipulation of BDDs. This development is a decision procedure certified in Coq that can be used using a reflexive approach for automatic proof in Coq [10].
- B. Werner investigated rewriting proofs using traces (generated by a CAML program or by the ELAN rewriting system). His method seems to give a good compromise between efficiency in time and space, while keeping a fully secure approach.

1.2 New libraries

A library of real numbers designed by M. Mayero has been integrated to the system.

2 Certification of programs

Jean-Christophe Filliatre improved his tactic Correctness [7] for generating proof obligations for imperative programs. He was able to certify several sorting algorithms working with arrays, including heapsort [6]

Jean Duprat completed a proof of safety for a distributed garbage collector [9].

3 Formalisms

We also continue more fondamental work on formalisms for the mechanisation of mathematics. Gilles Dowek together with Benjamin Werner in a joint work with Th. Hardin and C. Kirchner worked on formalisms integrating deduction and computation called Deduction systems modulo [4, 5]. We are currently working on a new type theory including modules (following the ideas developed by J. Courant [3]) and functions defined by reduction rules.

4 Animation

G. Dowek and C. Paulin, together with Y. Bertot and L. Thery organised the international conference TPHOLs'99 (Theorem proving in Higher-Order Logic) [2].

C. Paulin organised a Coq users meeting during the conference FM'99.

B. Werner presented the Coq system during the Types SummerSchool.

5 Collaborations

5.1 Nijmegen university

Freek Wiedijk from Nijmegen university visited our group at LRI during 2 weeks, in order to improve his knowledge of the internal structure of the Coq'system.

Herman Geuvers visited the INRIA site and presented his work on the fundamental theorem of Algebra.

5.2 INRIA Rocquencourt, ENS Lyon and LRI

The teams in the three sites have regular meetings.

5.3 INRIA Sophia-Antipolis

We collaborate with the INRIA Sophia-Antipolis site in the domain of Certified Computer Algebra and concerning the interaction between Coq and CtCoq.

5.4 Edinburgh

Pierre Courtieu is responsible of the interaction between Coq and the interface ProofGeneral developed by the Edinburgh site.

References

[1]: B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, H. Laulhère, P. Loiseleur, C. Muñoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual -- Version V6.3, July 1999.
[2]: Yves Bertot, Gilles Dowek, Christine Paulin-Mohring, and Laurent Théry, editors. International Conference on Theorem Proving in Higher Order Logics (TPHOLs'99), volume 1690 of LNCS. Nice, Springer-Verlag, September 1999.
[3]: Judicaël Courant. MC: A module calculus for Pure Type Systems. Research Report 1217, LRI, June 1999.
[4]: G. Dowek, Th. Hardin, and C. Kirchner. HOL-ls: an intentional first-order expression of higher-order logic. In P. Narendran and M. Rusinowitch, editors, Rewriting Techniques and Applications (RTA), number 1630 in LNCS, pages 317--331. Springer-Verlag, 1999.
[5]: G. Dowek and B. Werner. Proof normalization modulo. In Thorsten Altenkirch, Wolfgang Naraschewski, and Bernhard Reus, editors, Types for proofs and programs 1998, volume 1657 of LNCS. Springer-Verlag, 1999.
[6]: J.-C. Filliâtre and N. Magaud. Certification of Sorting Algorithms in the System Coq. In Theorem Proving in Higher Order Logics: Emerging Trends, 1999.
[7]: Jean-Christophe Filliâtre. Proof of Imperative Programs in Type Theory. In Thorsten Altenkirch, Wolfgang Naraschewski, and Bernhard Reus, editors, Types for proofs and programs 1998, volume 1657, 1999.
[8]: G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 6.3, July 1999.
[9]: Luc Moreau and Jean Duprat. A construction of distributed reference counting. Technical Report RR1999-18, LIP, 1999.
[10]: Kumar Neeraj Verma and Jean Goubault-Larrecq. Reflecting bdds in coq. Technical report, INRIA, December 1999.

This document was translated from L^AT_EX by H^EV^EA.

Next: INRIA Sophia-Antipolis Up: Progress Report Previous: Chalmers