Olivier Pons
30 ans- Célibataire
Dégagé des obligations militaires
(351) 96 41 86 407
Olivier.Pons@sophia.inria.fr
 Adresse permanente
1 Résidence Brune
Square A. Renoir
75014 Paris (France)
(33) 1.45.42.98.06
Situation actuelle:Chercheur à l' Universidade do Minho, (Portugal).

Formation

1999 Doctorat en Informatique
Conservatoire National des Arts et Métiers,
Titre :Conception et réalisation d'outils d'aide au développement de grosses théories dans les systèmes de preuves interactifs,
Jury : Yves Ledru, Gilles Dowek, Jean Goubault-Larrecq, Pierre Casteran, Jean Francois Monin, Yves Bertot, Laurence Rideau, Véronique Donzeau-Gouge.

1995 Diplôme d'études approfondies en Informatique (mention bien),
Université Pierre et Marie Curie (Paris 6)

1993 Maîtrise de Mathématiques Pures (mention Assez Bien),
Université Pierre et Marie Curie (Paris 6) et
Universitad Computense de Madrid (6 mois de stage ERASMUS)

1992 Licence de Mathématiques,
Université Pierre et Marie Curie (Paris 6)

1991 DEUG Science et structure de la matière,
Université Pierre et Marie Curie (Paris 6)

Séjour post-doctoral

Octobre/Novembre 1999 et depuis Septembre 2000 à l' université do Minho (Portugal),
dans l'équipe du Pr. Valença (Groupe Logique et Méthodes Formelles) .
Travail sur le sous typage et sur les isomorphismes de type
(avec Gilles Barthe, Maria-Joao Frade Luis Pinto).

Publications

Conférences internationales avec comité de lecture

    Olivier Pons. << Undoing and Managing a proof >>. Dans les actes de "User Interfaces for Theorem Provers 1997", Sophia-Antipolis, France, 1997.
    Accessible à l'URL: http://www.inria.fr/croap/events/uitp97-papers.html

    Olivier Pons, Yves Bertot, et Laurence Rideau. << Notions of dependency in proof assistants >>. Dans les actes de "User Interfaces for Theorem Provers 1998", Heindoven, Hollande 1998.
    Accessible à l'URL: http://www.win.tue.nl/cs/ipa/uitp/proceedings.html

    Olivier Pons. <<Proof generalization and proof reuse>>. TPHOL, Works in progress mars 2000
    Accessible à l'URL: ftp://ftp-sop.inria.fr/lemme/Olivier.Pons/generalisation.ps.gz

Conférences nationales avec comité de lecture

    Olivier Pons. <<Ingénierie de preuve>>. Dans les actes des "Journées francophones des langages applicatifs 2000", Mont Saint-Michel, France, 2000.
    Accessible à l'URL: http://pauillac.inria.fr/jfla/2000/actes.html


Autres Conférences

    Olivier Pons. <<Outils de navigation et de maintenance dans un script de preuve>>. Journée du GDR de programmation, Pôle Interfaces et Environnements Orléans, France, Novembre 1996.

Thèse

    Olivier Pons. << Conception et réalisation d'outils d'aide au développement de grosses théories dans les systèmes de preuves interactifs >>. Thèse de Doctorat, Conservatoire National des Arts et Métiers , 1999.
    Accessible a l'URL: http://www-mips.unice.fr/~pons/These/these.ps.gz.

Rapports Internes


    Olivier Pons. <<Proof engineering>>. rapport interne, Cedric 00/19 février 2000. (soumis à publication)
    Accessible à l'URL: ftp://ftp-sop.inria.fr/lemme/Olivier.Pons/tphol.ps.gz


    Yves Bertot et Olivier Pons. "Dependency graphs in theorem provers " à paraître comme Rapport technique Inria (Soumis à publication) octobre 2000.
    Accessible à l'URL: ftp://ftp-sop.inria.fr/lemme/Olivier.Pons/graphs.ps.gz

    Gilles Barthe et Olivier Ponse "Type Isomorphisms and Proof Reuse in Dependent Type Theory" à paraître comme Rapport technique Inria (Soumis à publication) . octobre 2000.
    Accessible à l'URL: ftp://ftp-sop.inria.fr/lemme/Olivier.Pons/reuse.ps.gz

    Gilles Barthe, Venanzio Capretta et Olivier Ponse "Setoids in type theory" à paraître comme Rapport technique Inria (Soumis à publication). novembre 2000.
    Accessible à l'URL: ftp://ftp-sop.inria.fr/lemme/Olivier.Pons/setoid.ps.gz

Autres Présentations

  Nov. 1996 Démonstration des outils de navigation et de maintenance d'un script
      de preuve au GDR de programmation à Orléans.
  Mars. 1998 Exposé au groupe BIP (séminaire commun CNAM, Paris 6)
      "Notions de dépendances dans le système Coq"
  Avril. 1998 Présentation à la conférence BRA Types 1998 à Kloster Irsee (Allemagne)
      ``Dependencies study in proof assistants".
  Juillet. 1998 Démonstration d'outils de visualisation et de manipulation de dépendances
      entre objets d'une théorie au colloque UITP'98 à Eindhoven
  Octobre. 1998 Exposé au groupe BIP (séminaire commun CNAM, Paris 6)
      "Transformations de preuve dans les systèmes ou la preuve est dirigée
      par les buts".


Réalisations pratiques

  • Outils de recherche dans une bibliothèque de fichier Coq (en Perl)
    ftp://ftp-sop.inria.fr/lemme/Olivier.Pons/coqfind

    Enseignement

    1999 -- 2000 Institut d'Informatique d'Entreprise
    A.T.E.R. à temps plein (192 h).
    Tous mes enseignements à l'IIE ont été effectués en première année.
    • Responsable du cours "Fondements de la programmation" ainsi que de deux groupes de TD, avec Caml comme support.
    • TD et TP d'"Algorithmique et programmation" (Cours Brigitte Grau), avec C comme support.
    • Suivi des projets de programmation (en C).

    1998 -- 1999 Conservatoire National des Arts et Métiers.
    Poste plein d'A.T.E.R.(192h)
    • TD et TP du cours "Algorithmique et Programmation"
      en cycle A (premier cycle) avec Ada comme support. (Cours V. Viguié Donzeau-Gouge).
    • Cours et TD du cours "Programmation et developpement orientes objets"
      en cycle B (second cycle) pour lequel j'ai enseigné Java et OCaml.

    1996 -- 1998 Université de Nice Sophia Antipolis.
    Vacataire.
    • TD du cours Objets Formels pour l'Informatique
      (cours de J.M. Fedou) en Deug MP2
      (24h 1996).
    • TD-TP de Scheme
      (Cours de J.P Roy) en Deug MI2
      (26h chaque année)

    • TD de Java
      en Licence-Maîtrise MASS
      (26h en 1996)
    • Responsable du cours et des TD de Java
      en Licence MASS
      (19h30 de cours et 43 h de TD en 1997)

    1996 -- 1997 Ecole Supérieure en Sciences Informatiques (ESSI)
    Vacataire.
    • TD-TP du Cours Sémantique des langages de programmation
      (Cours d'Isabelle Attali) au DEA d'Informatique de l'ESSI
      (12 h)

    Autre activité scientifique

    Depuis 1995 participation au Séminaire Interdisciplinaire Izotges regroupant de jeunes chercheurs de toutes disciplines (avec une dominante Mathématiques, Biologie, Philosophie). Le but de ce groupe, qui se réunit plusieurs week-ends par an et une semaine chaque été est de favoriser la communication inter-disciplines.