Next: Katholieke Univ. Nijmegen Up: Progress Report Previous: ENS Lyon and INRIA Rocquencourt

INRIA Sophia-Antipolis

Our research focuses mainly on four topics:

1) User interfaces for proof assistants,

2) Specifications and proofs of properties of programming langages,

3) Certified computer algebra,

4) Type Theory (allowing recursion on functional terms).

Annual report.

Pierre Corbineau, in a master work, has completed a proof of correctness of an imperative programs in Coq. The program, a control algorithm for n lifts, is one of the typical examples for which the B method is particularly well suited. We have used there a method recently implemented in Coq by Jean-Christophe Filliatre, from the Inria rocquencourt site, who has given a valuable help on the use of his system.

Joelle Despeyroux has presented her joint work with Pierre Leleu on Primitive recursion for higher-order abstract syntax with dependant types at the FLoC'99 Intuitionistic Modal Logic with Applications workshop, in July 99, in Trento, Italy. A paper has been submitted to a journal.

Guillaume Gillard has made some experiments on using a technique of representation of variables due to Andrew Gordon to formalize a concurrent and object calculus up to alpha-conversion in Coq. This method is intermediate between the use of de Bruijn codes, and the use of higher-order abstract syntax. It leads to specifications and proofs relatively closed to work on paper, much shorter and readable than when using de Bruijn codes.

Etienne Lozes, in a master work, has proposed several proofs of correctness of a new Coq algorithm for inference of types, using the extraction mechanism and different encodings of bind variables. This experiment has been very rich. In particular, we hope to extend two of the tested approches to larger languages or calculi, such that the one chosen by Guillaume Gillard.

Yves Bertot has completed in Coq an industrial problem previouly solved with the B method. The goal was to understand how dependant types and the CCI was useful in specification and analysis of programs.

Antonia Balaa, during her PhD, studies tools helping reasonning on functions defined by well-founded induction. As a case study, she has developped in Coq some algorithms on graphs (e.g. minimal spanning tree).

Laurent Théry has adapted the initial proof of Stålmarck algorithm, replacing lists by structures with handlers, to optimize the extracted code.

In his <>, Benoit Frondas has developped a method for reasonning about the complexity of a program inside Coq. With a prototype of this method, he has then proved an insertion sort implementation and its time complexity.

During his third year of Ecole Polytechnique, Virgile Prevosto has made at Sophia an experimental implementation of an extraction method from Coq to Java, tested with succes on a cryptographic algorithm. One of the main problem was to translate inductive types into classes.

Henrik Persson, with a result of his PhD, has integrated a constructive proof of Dickson lemme in the developpement of Laurent Théry of the Buchberger algorithm, and tested the extracted code in Ocaml.

Starting from a suggestion of N.G.De Bruijn, Loïc Pottier has developped a theory of telescopes in Coq. The goal is to give a foundation in type theory of the representation of mathematical structures.

Laurent Chicli has begun the formalization of sheme theory in Coq (topology, sheaves, local rings).

Frédérique Guilhot has made a formalization in Coq of matrices, based on the course of André Hirschowitz at University of Nice.

The Ctcoq interface to Coq has been translated into Java, using the Aioli and Figue tools. This Java implementation is called Pcoq, and will be ready at the end of the year (Pascal Lequang, Yves Bertot, Laurence Rideau, Loïc Pottier). It includes many novelties, among them a true 2D rendering of formulas (indices, fractions, roots).


Four people from our site attended the annual TYPES meeting held at Lokeberg in Sweden in June 99; Two of them gave a talk there.

Three PhD students from our site attended the Types Summer School held in Giens in September 99. Five researchers were there as free participants.

The Sophia site has organized a summer school on Theory and Practice of Formal Proofs at Giens, France, from August 30 to September 10, 1999. There has been 55 participants, mainly PhD students (34), but also researchers (14) and ingeneers (7). About 10 people attend the school as free participants.

Some references.

Yves Bertot, "Des environnements de preuve aux environnements de programmation", Habilitation à diriger des recherches, October 1999.

Yves Bertot, "The Ctcoq system: Design and Architecture", Formal Aspect of computing, 1999, vol 11 pp225-243.

Yves Bertot, "Ctcoq et PCoq", FM'99, Toulouse, "colloque satellite des utilisateurs de Coq", September 1999.

Joëlle Despeyroux and Pierre Leleu. Recursion over Objects of Functional Type. Journal version, Submitted for publication, Sept 99.

Guillaume Gillard. A formalization of a concurrent object calculus up to alpha-conversion. Submited for publication, Dec 99.

Olivier Pons, "Conception et réalisation d'outils d'aide au développement de grosses théories dans les systèmes de preuve interactifs", PhD thesis, CNAM, July 1999.

Loïc Pottier, "Un début de formalisation de l'algèbre en Coq et Ctcoq", INRIA Research Report, 1999.

Loïc Pottier, "Formalization of algebra in Coq and Ctcoq", workshop Types, Lökegerg, June 1999.

Loïc Pottier, "La contrib algebra de Coq", M'99, Toulouse, "colloque satellite des utilisateurs de Coq", September 1999.

Laurent Théry and John R. Harrison", A Skeptic Approach to Combining HOL and Maple", Journal of Autmated Reasoning" 1998, vol 21 no 3 pp 295-325.

Next: Katholieke Univ. Nijmegen Up: Progress Report Previous: ENS Lyon and INRIA Rocquencourt