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).
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 <
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).
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.
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.
Meetings.
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.
Some references.
Yves Bertot, "Des environnements de preuve aux environnements de
programmation", Habilitation à diriger des recherches, October 1999.
Next: Katholieke Univ. Nijmegen
Up: Progress Report
Previous: ENS Lyon and INRIA Rocquencourt