Yves Bertot's research activity

La même page en Français.

Summary

Most of my current research revolves around the objective of developing provably correct software. There is a strong emphasis on software for programming languages (partial evaluation, compilation, byte-code verification), as embodied in the Verificard project, for which we were awarded funding by the european community. I also studied software from other branches of computer science like large number arithmetic or computational geometry.

Provably correct software means that programs come with proofs of correctness. In my work all these proofs are verified mechanically using an interactive theorem prover. Some of my research therefore also focusses on the usability of these theorem provers, especially theorem provers based on type theory. I've worked on making certain classes of recursive functions easier to use and I have worked on re-using proofs.

I have also studied the tools needed in the proof developer's working environment, to make tractable the construction of the large documents that describe a program and the proof of its correctness. This results in graphical user interfaces for the theorem prover Coq, now developed in collaboration with all members of the Lemme team at INRIA Sophia Antipolis.

a book on Coq (in French), All publications, Access to the main papers, Access to the main software contributions, Teaching (in french), Curriculum Vitae, Past research activities, Programming hot-list, A very short formalized proof that the square root of 2 is not rational

Main topics of my research activities

Performing proofs using the Coq system

I am an intensive user of proof systems, mainly the Coq system, for which I also developed a working environment (see pcoq below). I have used Coq to perform very large proofs in the domain of programming language semantics, for instance the correctness proofs for a program transformation tool, a compiler, and an abstract byte code verifier. More recent work leads to a description of the relation between natural semantics and denotational semantics that is better amenable to formalization in type-theory than usual domain-theoretic presentations. I am also interested in 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 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 the Université de Paris-Sud), general recursion, partial evaluation, etc.

In the experiments developed in the Lemme team, we have discovered several aspects of type-theory based systems that needed some further theoretical investigations. One study, done with Antonia Balaa attempts to make the use of general recusion easier by studying the fixpoint equations, for some classes of recursive functions. Another study, done with Nicolas Magaud, attempts to make proofs less sensitive to representation choices for data structures.

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 TPHOLS'2000 conference. You can find a copy of the slides I used for this occasion, at the following location (compressed tar archive) I also teach Coq at the university of Nice. You can see my course notes, in French, at the following address. Last, I am participating on writing a book for users of the coq system, you can access to some material (in French) through this link

Working Environments for Proof systems: the CtCoq and pcoq systems,

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. 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 techniques have been experimented with first by L. Théry. The paper published at SDE5, coauthored with Gilles Kahn and myself, 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 proof management, 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, and 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.

Another successful system that took advantage of the ideas developed in our user-interfaces is Proof General, a theorem prover user-interface developed on top of XEmacs. I collaborated with that system's developers in 1996 (see this report) and they have happily re-used our ideas on proof-by-pointing and script management (see this link for their reference to our work).

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. The main functionalities developed in this work are described in this paper. 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.

Past research activities

My research started in the CROAP team, under the supervision of Gilles Kahn. At that time the team was developing a large interactive programming environment generator, called Centaur. Centaur contained tools to describe the syntax of programming languages (based on Yacc), the way programs should be displayed, and the semantics of programming languages. I studied how a parallel programming language could be handled in this environment. This required some enhancements to the Centaur system, since my experience was the first experience of describing a parallel programming language in a generic programming environment generator like Centaur. In particular, I studied the animation of program execution, where instructions could be highlighted as execution progressed. The novelty was that several instructions needed to be highlighted at once, because of parallelism.

This experience with a parallel programming language led to my Ph.D thesis, where I described how the highlighting information could be synthesized automatically from the dynamic semantics of the programming language, when this semantics was described using Natural Semantics à la Gilles Kahn or Structural Operational Semantics à la Gordon Plotkin.

I then studied the applicability of programming environments to other computer related activities, like proof development. This topic is still active for me and my team. On the other hand, I had developed a strong competence on the formal description of programming language. I continued this research by studying how formal descriptions could be used to show the correctness of programming tools like type-checkers, compilers, or program transformation tools and verify these proofs mechanically. This topic also continues to be active for me and my team.

Publications

Note: these publications are listed in reverse chronological order. Click here to see recent research reports

Les publication sont énumérées dans l'ordre chronologique inverse, mais les rapports de recherche apparaissent à la fin

Yves Bertot Filters on CoInductive Streams, an Application to Eratosthenes' Sieve , Proceedings of TLCA'05, Springer LNCS 3461, 2005. A preliminary version is available as INRIA research report RR-5343, The corresponding source code is also available.

Yves Bertot, Pierre Castéran
Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer Verlag, EATCS Texts in Theoretical Computer Science, ISBN 3-540-20854-2 (associated internet site).

Milad Niqui, Yves Bertot
``QArith: Coq Formalization of Lazy Rational Arithmetic", Types 2003, LNCS 3085.

Y. Bertot, F. Guilhot, Loïc Pottier
Visualizing Geometrical Statements with GeoView, Proceedings of the Workshop User Interfaces for Theorem Provers in connection withTPHOLs'2003, Rome, Italy, September 2003

Yves Bertot
``Simple canonical representation of rational numbers'', Mathematics, Logic and Computation, ENTCS Volume 85.7, September 2003.

Yves Bertot, Nicolas Magaud, and Paul Zimmermann
``A Proof of GMP Square Root'', Journal of Automated Reasoning 29(3-4):225-252, 2002. Special Issue on Automating and Mechanising Mathematics: In honour of N.G. de Bruijn (an earlier version is available as a research report).

Yves Bertot, Venanzio Capretta, and Kuntal Das Barman
`` Type-theoretic functional semantics '', TPHOLs'2002, LNCS 2410, pp. 83-98.

Yves Bertot,
`` Des descriptions fonctionnelles aux implémentations impératives de programmes'', Proceedings of Journées francophones des langages applicatifs, JFLA'02, INRIA (in French).

Antonia Balaa and Yves Bertot,
`` Fonctions récursives générales par itération en théorie des types'', Proceedings of Journées francophones des langages applicatifs, JFLA'02, INRIA (in French).

David Pichardie and Yves Bertot,
`` Formalizing Convex Hulls Algorithms '', Proceedings of TPHOLs'01, LNCS 2152, pp. 346-361.

Ahmed Amerkad, Yves Bertot, Laurence Rideau, and Loïc Pottier,
`` Mathematics and proof presentation in Pcoq'', Proceedings of Proof Transformation and Presentation and Proof Complexities (PTP'01), Sienna, Italy.

Yves Bertot
`` Formalizing a JVML verifier for initialization in a theorem prover '', Proceedings of CAV'01, LNCS 2102, pp. 14--24, July 2001.
short version of INRIA Research Report RR-4047, November 2000.

Nicolas Magaud and Yves Bertot,
``Changing Data Structures in Type Theory: A Study of Natural Numbers'', Proceedings of Types2000, LNCS 2277, pp. 181-196.

Antonia Balaa and Yves Bertot,
``Fix-point Equations for Well-Founded Recursion in Type Theory'', Proceedings of TPHOLs'2000, LNCS 1869, 2000.

Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin, and Laurent Théry,
Theorem Proving in Higher Order Logics (TPHOLs99), volume 1690 of Lecture Notes on Computer Science, Springer Verlag, Nice, France, September, 1999.

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).

Research Reports

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 and Olivier Pons and Loïc Pottier
`` Dependency graphs for interactive theorem provers''
INRIA Research Report RR-4052, November 2000.

Yves Bertot
`` A Coq Formalization of a Type Checker for Object Initialization in the Java Virtual Machine''
INRIA Research Report RR-4047, November 2000.

Yves Bertot and Nicolas Magaud and Paul Zimmermann
`` A proof of GMP square root using the Coq assistant''
INRIA Research Report RR-4475, June 2002.