Animations: Interactive proof using the mouse
(24MBytes, mpeg),
Drag
and drop for algebraic manipulations (39 KBytes, mpeg).
la même page en français
Animations: Interactive proof using the mouse
(24MBytes, mpeg),
Drag
and drop for algebraic manipulations (39 KBytes, mpeg).
Most of my research activities were hosted in the CROAP project.
I am an intensive user of proof systems, mainly the Coq system, for which I also developed a working environment (see CtCoq below). I have used Coq to perform very large proofs around programming language semantics, but I also got interested into finite group theory and geometric algorithms.
What fascinates me with Coq is that this system is becoming a real programming language, and I want to see how far we can go in terms of developing certified but efficient programs for a large spectrum of computer applications. If such a large spectrum of computer applications is to be covered, then all kinds of program development techniques must be applied: imperative features (but this is already studied by colleagues like Jean-Christophe Filliatre at Université de Paris-Sud), general recursion, partial evaluation, etc.
In the experiments developed in the Lemme team, we have discovered that general recursion, provided in Coq in the form of well-founded recursion was especially difficult to use. With Antonia Balaa we have studied ways to make this problem simpler. This has led to a publication on fixpoint equations.
After long years of practice, I have a good knowledge of the Coq system, and I have been invited to give a tutorial on this system at the TPHOL'2000 conference. You can find a copy of the slides I used for this occasion, at the following locations (compressed tar archive), (postscript file). I also teach Coq at the university of Nice. You can see my course notes, in French, at the following address.
Working environments for proof systems are similar to programming environments. The study of programming environments was the main subject of study in the CROAP group at INRIA-Sophia Antipolis where I was trained (see below work on Centaur), and which I directed from 1994 to 1998.where I was trained and The Centaur system can also be used to define formally the syntax and layout of command languages for proof systems. These definitions can then be used to construct language-specific tools that will also be hosted in the Centaur system. Using inter-process communication techniques, it is then possible to connect the language specific tools directly with the proof system. These technique have been first experimented by L. Théry. The paper SDE5 describes these techniques.
Using these techniques, I have designed a working environment for the Coq system, called CtCoq. In this environment, we have experimented with various ways of using the mouse to guide the proof process, with techniques to keep a clean trace of the work done during the session, with techniques to backtrack gracefully when early errors are discovered in the design of a proof. Papers related to these topics are TACS94, UITP97, JSC. Recent work on this topic includes a re-implementation in Java of these ideas, based on libraries for structured manipulation, aioli, and display, figue. This new implementation is called pcoq.
In these graphical user-interfaces we have studied several techniques to guide the proof process using mouse interaction. The first one is called proof-by-pointing, the second one I called drag-and-drop Rewrite. To know more about this technique, you can have a look at an animation I made to demonstrate its use (it is a 15MBytes Mpeg file). In this demonstration, expressions that appear in pink and green correspond to drag-and-drop movements performed by the user.
The next challenge I see in this domain is to provide help for the maintenance of large proofs: how to minimize the work to re-do when the specifications change only slightly? What kind of tools should be provided? How can these tools be integrated in the proving environment? In this domain, I have helped a former student of mine, Olivier Pons in his study of the use of graphs to visualize the structure of proof developments. Follow this link to see what I learned about dotty, a graph displaying and editing tool.
To exchange ideas around this topic, I have been participating in a series of workshop on User-Interfaces for Theorem Provers. I organized the 1997 venue. There were 30 attendants and 14 speakers. I also participated in the organization of the conference TPHOLs'99, which was held in Nice, in September 1999.
The CROAP group has developped a strong competence in the generation of language-specific programming environments based on formal descriptions of the programming languages. The formal descriptions encompass syntactical aspects, such as context-free grammars and layout descriptions, and semantic aspects, such as type discipline, operational semantics, or traduction to other languages.
It is possible to derive language specific tools from these formal descriptions: parsers from the grammar, pretty-printers from the layout specification, type-checkers, interpreters, or compilers from the semantic descriptions. The CROAP group has devised a generic system, called Centaur, that can be used to combine all these tools into a programming environment. Of course, Centaur is used as a language specific tool for the grammar, layout, and semantics formalisms. So it can be used both to define formally new tools and to run these tools.
In the Centaur system, I have been involved mostly with the semantics formalism: I have devised a technique, called subject tracking, that makes it possible to locate positions in programs during the execution of semantics specification. This technique is instrumental if one wants to animate programs or provide break-points in the interpreter generated from the formal specification. This technique and its applications is described in the papers ESOP90, PLDI91, CAAP92, and Logical Environments93.
There is an official tutorial for Centaur, but I also designed my own example around a language little, which I also use as a basis for proving properties of the programming language and develop certified analysis or transformation tools on programs (see below). The complete Centaur description of little is available here. It also contains mechanically checked proofs, but these were done with an old version of the Coq system.
Along the years, I developped a small set of tools to make it easier to use Centaur. Most predictably, there will not be any new release of that system in the near future, so I am making these tools available through a simple web-page.
The formal semantics of programming languages also make it possible to perform proofs on the behavior of programs in these languages. The semantic description technique is most useful to prove properties of language-specific tools. For instance, we have proved the correctness of a little partial evaluator for a simple imperative language. This work is described in TAPSOFT95.
These proofs on programming language semantics showed that there was a need to add more powerful tactics in the Coq system. I am currently designing these tactics and hope to be able to present them soon in a conference.
I also teach programming language semantics at the University of Nice. My course notes are in French, but you can see them at the following address. Note that I also use the interactive proof system Jape.
The Centaur system is aging. Other members of the CROAP team have already made a significant effort to develop a replacement system, that will be portable across more platforms (it will be written in Java) and less bundled (it will have clearer interfaces between independent modules). I am now studying how a new user-interface, now named pcoq can be built upon these tools .
I would like to know more about proofs of compilers (I did a little one, completely formally, for a small imperative language. Click here to have it), like that of Guttman, Wand and others at Northeastern University and Mitre Corporation
Following the evolution of the Coq system, I would like CtCoq to become a really practical tool for the development of certified programs. Right now, members of the new LEMME team are studying computer algebra algorithms. The size of the proofs they perform is a real challenge for the CtCoq system.
Note: these publications are listed in reverse chronological order. Click here to see recent research reports
Antonia Balaa and Yves Bertot,
Fix-point
Equations for Well-Founded Recursion in Type Theory'',
proceedings of TPHOLs'2000, LNCS 1869, 2000.
Yves Bertot,
"The CtCoq System: Design and
Architecture",
Formal aspects of Computing, Vol. 11, pp. 225-243, 1999.
Yves Bertot and Laurent Théry,
``A Generic Approach to Building User Interfaces for Theorem Provers'',
the Journal of Symbolic Computation Vol. 25, pp. 161-194, 1998.
Yves Bertot,
"Head-tactics simplification".
Algebraic Methodology and Software Technology, volume 1349 of
Lecture Notes on Computer Science, Springer Verlag,
Sydney, Australia, december,
1997.
Yves Bertot,
Direct manipulation of Algebraic Formulae in Interactive Proof Systems
,
Workshop on
User-Interfaces for Theorem Provers, September 1997.
Janet Bertot and Yves Bertot,
"CtCoq: a system presentation",
Automated Deduction (CADE-13), volume 1104 of Lecture Notes in
Artificial Intelligence, Springer-Verlag,
New Brunswick, NJ, USA, July 1996
Janet Bertot and Yves Bertot,
"The CtCoq experience",
User Interfaces for Theorem Provers'96,
York (UK), July 1996.
Yves Bertot and Ranan Fraer,
"Reasoning with Executable Specifications",
International Joint Conference of Theory and Practice of
Software Development (TAPSOFT/FASE'95) , Springer-Verlag LNCS 915,
Aarhus (Denmark), May 1995.
Yves Bertot, Gilles Kahn, and Laurent Théry,
``Proof by Pointing'',
Symposium on Theoretical Aspects Computer Software (STACS),
Sendai (Japan), LNCS 789, April 1994.
Also appears as Cambridge University Research Report (December 1993).
Laurent Théry, Yves Bertot, and Gilles Kahn,
``Real Theorem Provers Deserve Real User-Interfaces''
The Fifth ACM Symposium on Software Development Environments (SDE5),
Washington D. C., December 1992.
Also appears as Inria Research Report no. 1684 (May 1992).
Yves Bertot,
``A Canonical Calculus of Residuals'',
In Logical Environments, Gerard Huet and Gordon Plotkin, editors,
Cambridge University Press, December 1993.
Yves Bertot,
``Origin Functions in Lambda-calculus and Term Rewriting Systems'',
Proceedings of CAAP'92, Caen (France), February 1992.
Also appears as Inria Research Report no. 1543 (October 1991).
Y. Bertot,
``Occurrences in Debugger Specifications'',
Proceedings of the 1991 ACM SIGPLAN Programming Language Design and
Implementation (PLDI) Conference, Toronto, June 1991.
Also appears as Inria Research Report no. 1350 (December 1990).
Yves Bertot,
``Implementation of an Interpreter for a Parallel Language in Centaur''
,
3rd European Symposium on Programming, Copenhague, Denmark,
LNCS 432, May 1990.
Also appears as Inria Research Report
no. 1076 (August 1989).
Yves Bertot,
Programming Languages Specifications and Environments
A course on describing programming languages for the Centaur
environment and proving properties of these languages,
INRIA Research Report RT-210,
December 1997.
Janet Bertot, Yves Bertot, Yann Coscoy, Healfdene Goguen, and
Francis Montagnac,
INRIA Research Report RT-210,
User Guide to the CtCoq Proof Environment,
October 1997.
Yves Bertot, Thomas Kleymann-Schreiber, Dilip Sequeira,
Implementing Proof by Pointing without a Structure Editor
INRIA Research Report RR-3286, October 1997.
Yves Bertot,
A certified compiler for an imperative language
INRIA Research Report RR-3488, September 1998.
Yves Bertot,
The CtCoq System: Design and Architecture
INRIA Research Report RR-3540, October 1998.