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 :

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.


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.

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.

Judicaël Courant. MC: A module calculus for Pure Type Systems. Research Report 1217, LRI, June 1999.

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.

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.

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.

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.

G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 6.3, July 1999.

Luc Moreau and Jean Duprat. A construction of distributed reference counting. Technical Report RR1999-18, LIP, 1999.

Kumar Neeraj Verma and Jean Goubault-Larrecq. Reflecting bdds in coq. Technical report, INRIA, December 1999.

This document was translated from LATEX by HEVEA.

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