In the area of implementation of tools, let us mainly quote the continuation of the work of Yann Coscoy on the translation of proof terms in a pseudo natural language (Cos96). The generated texts are now both more compact and clearer. The system is distributed both for Coq and for CtCoq.
In the area of applications, Loic Pottier et Laurent Théry have started a new activity on program certification applied to symbolic computation. The goal is to develop a certified library for symbolic computation on polynomials. A first step has been to develop a proof of the Buchberger's algorithm in the Coq proof assistant. The formulation of the algorithm can then be efficiently compiled and used to do computation.
Finally, in the area of refinement of Type Theories, we find the work by Joëlle Despeyroux and Pierre Leleu. In a first step towards reconciling higher-order abstract syntax with induction, Joëlle Despeyroux, Frank Pfenning and Carsten Schürmann have proposed (DPS97) a system -an extension of the simply-typed lambda-calculus- that permits iteration and case reasoning over subjects of functional type. Pierre Leleu, as part of his PhD thesis, now proposes an improved version of this system, with the hope to extend it to polymorphic or dependent types. (Draft paper to be submitted soon.)
Visits between the sites:
Yves Bertot visited the Edinburgh site, 3-9 November 1996, to help implementing the proof-by-pointing strategy in Lego under XEmacs.
Some references:
Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor. Technical Report ECS-LFCS-97-368, University of Edinburgh, Also appears as INRIA Research Report RR 3286, 1997. http://www.inria.fr/RRRT/RR-3286.html.
Janet Bertot, Yves Bertot, Yann Coscoy, Healfdene Goguen, and Francis Montagnac. User guide to the CtCoq proof environment, October 1997. Rapport technique INRIA, RT-0210.
Yann Coscoy. A natural language explanation for formal proofs. In C. Retoré, editor, Proceedings of International Conference on Logical Aspects of Computational Liguistics (LACL), Nancy, volume 1328, pages 149-167. Springer-Verlag LNCS/LNAI, September 1996.
Joëlle Despeyroux. Sémantique Naturelle: Spécifications et Preuves. Graduate course in the DEA Mathématiques Discrètes et Fondements de l'Informatique (MDFI), Marseille, 1995-1997, unpublished lecture notes, 70 pages, in french, December 1997. http://www.inria.fr/croap/personnel/Joelle.Despeyroux/Joelle.html,
Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In Philippe de Groote and J. Roger Hindley, editors, Proceedings of the 3rd Int. Conference on Typed Lambda Calculi and Applications, TLCA'97, Nancy, France, April 2-4, pages 147-163. Springer-Verlag LNCS 1210, April 1997. An extended version is available as CMU Technical Report CMU-CS-96-172.
Amy Felty and Laurent Théry. Interactive Theorem Proving with Temporal Logic. Journal of Symbolic Computation, volume 23, April 1997, pages 367-397.
Pierre Leleu. A modal lambda-calcul with iteration and case constructs. To appear as an Inria research report, December 1997.
Olivier Pons. Undoing and Managing a proof. In Proceedings of User Interfaces for Theorem Provers 1997, Sophia Antipolis, France, September 1997. electronic notes. http://www.inria.fr/croap/events/uitp97-papers.html.
Laurent Théry. Proving and computing: a certified version of the buchberger's algorithm. rapport de recherche 3275, INRIA, October 1997.