Thèmes de recherche

• Systèmes formels et environnements de développement.:
  Je travaille à la réalisation d'outils d'aide au développement de grosses théories pour les systèmes d'aide à la preuve comme Coq, Lego, Hol, Isabelle ou PVS. Le but est de fournir des outils permettant de mieux comprendre de grosses preuves, de gérer les dépendances entres des sous-preuves ou entre les différents résultats mathématiques afin de faciliter les développement et la maintenance. Un exemple de grosse preuve, qui a servie de base d'expérimentation, est la preuve (constructive) du théorème de Buchberger réalisé en coq par Laurent Thery
  
  
• Théorie des types: J'ai travaillé dernièrement avec Gilles Barthe sur les isomorphismes de type. Nous avons tenté de présenter panorama de situations ou (une interprétation calculatoire des) isomorphismes de type permet la réutilisation de preuve. Nous proposons une extension des systèmes de types dépendants ou les isomorphisme de type sont capturé par des règles de réécriture au niveaux des type et des termes.
  
  Je m'intéresse aussi au problèmes de sous-typage et plus particulièrement au sous-typage par constructeur qui est une forme basique de sous-typage dans laquelle un type inductif s est vu comme un sous-type d'un type inductif t si t a plus d'habitants que s. C'est le cas si tout constructeur de s est aussi un constructeur de t.

Enseignement

Publications récentes

• 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 generalization and proof reuse" TPHOL, Works in progress 2000. mars 2000.
  
• Yves Bertotet Olivier Pons
  "Dependency graphs in theorem provers", à paraître comme Rapport technique Inria (Soumis à publication) octobre 2000.
  
• Gilles Barthe et Olivier Pons. "Type Isomorphisms and Proof Reuse in Dependent Type Theory" à paraître comme Rapport technique Inria (Soumis à publication) octobre 2000.
  
• Gilles Barthe,Venanzio Capretta et Olivier Pons "Setoids in type theory" (Soumis à publication) novembre 2000.
• Olivier Pons
  "Proof engineering" rapport interne, Cedric 00/19 février 2000.
  
• Olivier Pons
  "vers une formalisation de l'algèbre relationel en coq", Rapport de DEA (j'ai un peu honte mais ça peut remonter le moral de ceux qui rament en DEA !)

Quelques réalisations pratiques

• Outils de visualisation des dépendances basés sur les systèmes de visualisation de graphes daVinci et Dotty.
  
  1. coq-graphs
     
  2.  dependtohtml : un programme pour créer une page html  représentant  un graphe orienté, où  les noeuds sont cliquables.
• Recherche dans une bibliothèque de fichiers Coq
  Un petit script PERL pour fouiller les bibliothèques de Coq:
  coqfind,(c'était vraiment mon premier script Perl, mais ça marche bien et MOI je l'utilise abondamment)

Un mode emacs (pour XEmacs 19.13 et suivant) pour Coq (obsolètes!)

• coq.el,
  
• inf-coq.el,
  
• La doc,