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 LATEX by HEVEA.
Next: INRIA Sophia-Antipolis
Up: Progress Report
Previous: Chalmers