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 assistant in 1997 and 1998 at University of Nice Sophia Antipolis.
    (more information in french)


    Some small hacks (sometime obsoletes !)

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


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

    Some usefulls links