Olivier PONS

  • Equip: Lemme at Inria Sophia Antipolis and,
  • Equip: Logic and Formal Methods at Universidade do Minho ,
  • Phones: (351) 96 41 86 407 (mobile in Portugal)

  • (351) 253 60 44 61 (Universidade do Minho)
  • Fax: +33 92 34 76 33 (Inria lemme project)
  • E-mail: Olivier.Pons@sophia.inria.fr

  • This page is perpetually under construction

    This page may be out of date for more information on publications, and working activity see the French version

    my English is too bad...do not hesitate to send me correction...!
    I graduated (July 99) a PhD Thesis from the Conservatoire National des Arts et Métiers in France. Im a m now in post doctoral position a the university of minho (Portugal). For the past four years, I have been working with Yves Bertot, and Laurence Rideau in the CROAP project at INRIA. My thesis supervisor was Véronique Donzeau-Gouge from the CEDRIC team of CNAM. 

    Research Interests

    If somebody could correct the english of this brief resume of my thesis....

    This thesis aims at providing tools to improve the productivity of users of interactive proof systems such as Coq system, HOL or PVS. Such tools are particularly needed for the development of large theories and, based on various notions of dependencies, they apply to the development and maintenance activities. In the first part, we present tools that help in understanding and restructuring proofs. Possibilities include : the graphic visualization of the proof tree, visualization and the navigation in the textual representation of the proof script, a logical undo-redo (that suppresses a command of the proof script without affecting parts of the proof logically independent of the command to erase), the contraction and the expansion of a proof script (using tacticals), and finally the extraction of a sub-proof from a demonstration in order to produce a stand alone lemma. In the second part, we describe tools for the restructuring of theories. To implement them we have written a program that analyses the dependencies between the results which constitute a development. Proposed tools include : the graphic visualization of the dependency graph, the slicing of the theories (the notion of slice is inspired from the notion used in programming languages and is defined as the least set of theorems that are needed to prove a result), the "logical reset" (analogous a t the level of theories of the logical undo of the first part), the reorganizati on of results by code motion, and an interactive help to the propagation of modi fications. In the last chapter we examine, by the way of examples, various methods for helping in the generalization of theorems and theories. We developed a prototype implementations of this tools using Coq and its graphical interface CtCoq, nevertheless, presented ideas are generic. 


    I was teaching associate (Vacataire) two years at the Universités of Nice Sophia Antipolis and at the Ecole Supérieure en Sciences Informatiques (ESSI) . During the year 1998-99 I was assistant professor (ATER) at the Conservatoire des Arts et Métiers then in 1999-2000 At the IIE engineering school.
    Some residues of my lesson available on line (in french) 

    Recent publications

    Some hacks (sometime obsolete !)

    An emacs mode (for XEmacs 19.13 et latter) for Coq (obsolete!)