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
-
Formal systems and Interactive Proof Environment.
(see the resume of my thesis below !)
-
Type Theory : Recently, I worked with Gilles Barthe
on type isomorphisms. We tried to present a panorama of situations where
(a computational interpretation of) type isomorphisms allows proof reuse.
We propose an extension of the dependent types system in wich type isomorphisms
are captured by rewriting rules at types and terms levels.
I am also interested in subtiping and more particularly
in constructor subtyping which is a basic form of subtyping in which an
inductive type S is seen like a subtype of an
inductive type T if T has
more inhabitants than S . It is the case if
any constructor of S is also a constructor of
T .
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.
Teaching
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
-
Olivier Pons
"
Ingénierie de preuve",Journées francophones des langages
applicatifs 2000", Mont Saint-Michel, France, 2000.
-
Olivier Pons. Conception
et réalisation d'outils d'aide au développement de grosses
théories dans les systèmes de preuves interactifs , PhD
Thesis,Conservatoire National des Arts et Métiers , 1999.
-
Olivier Pons, Yves bertot, Laurence Rideau
"Notions
of dependency in proof assistants", User Interfaces for Theorem Provers
1998.
-
Oliver Pons,
"Undoing
ans managing a Proof", User Interfaces for Theorem Provers 1997,
-
Olivier Pons
Proof
reuse generalization and proof " TPHOL, Works in progress 2000. March
2000 .
-
Yves Bertot and Olivier Pons
"
Dependency graphs in theorem provers " , to appear as Inria technical
report (Submitted) October 2000 .
-
Gilles Barthe and Olivier Pons .
"
Standard Isomorphisms and Proof Reuse in Standard Dependent Theory " .
"to appear in the proceeding of "Foundations of Software Science and Computation
Structures" (Fossacs'2001)
-
Gilles Barthe , Venanzio Capretta and Olivier
Pons "
Setoids in theory type " (Submitted) November 2000 .
-
Olivier Pons
"
Proof engineering " internal report/ratio, Cedric February 00/19
2000 .
-
Olivier Pons
"vers
une formalisation de l'algèbre relationel en coq", Rapport de
DEA (I was young... !!!)
Some hacks (sometime
obsolete !)
-
Tools to visualize dependency graphs based on the graphs
displaying system daVinci and
Dotty
.
-
coq-graphs
-
dependtohtml : a program to create a page HTML representing
a directed graph, where the nodes are cliquables.
-
Search a definition in a Coq library
A
small script Perl to find a Coq definition in the libraries. It can browse
your on library as soon as the Coq contrib. When the definition is found
the result pops in a new windows. Try it...
coqfind
, (It was really my first script Perl, but it works well and 'ME',
I use it abundantly)
An emacs mode (for XEmacs 19.13 et latter) for Coq (obsolete!)
