Olivier PONS

Organisation: INRIA

Research Unit: Sophia Antipolis

Project: CROAP

Tel : +33 4 92 38 76 32

Fax : +33 4 92 34 76 33

E-mail: Olivier.Pons@sophia.inria.fr

This page is perpetually under construction !

Research Interests

I'm currently doing a Ph.D. in Theoretical Computer Science at Inria Sophia-antipolis in the Croap project and in the Conservatoire des Arts et Metiers in the programming team. My Ph.D. is supervised by Yves Bertot, Laurence Rideau and Véronique Donzeau-Gouge.

My Ph.D. thesis

My Ph.D. work consists in the conception and the realization of tools providing help in the development and maintenance of large proofs and theories in proof assistant. The main develpment is done for the système Coq. and its interface CtCoq. We develop tools allowing to understand better the proof strategy in large proof and development, to manage the dependencies between sub-proofs and between mathematical results. We use this dependencies to help the user in all maintenance task (propagation of modifications, code motion, reorganization ...).

Others research interest

Teaching

Teaching assistant in 1997 and 1998 at University of Nice Sophia Antipolis.
(more information in french)

Publications

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
"vers une formalisation de l'algèbre relationel en coq" Master's report University Pierre et Marie Curie (Paris 6)

Some small hacks (sometime obsoletes !)

An emacs mode for Coq (for XEmacs 19.13 and latter)

Coqfind

A small Perl script to serach in the Coq library. coqfind,,(it was my first try in Perl !)