Au cnam

à Gobelins

Web avancé dans le cadre du mastère : Interactive digital experiences

Projets actuels:

Anciens projets:

Pour une liste à jours

[1] Jean-Ferdinand Susini, Olivier Pons, Nolwenn Guedin et Catherine Thevenot. Danse-doigts, jeu de motricité fine, Actes du 9 ème congrès sur les aides techniques pour les personnes Handicap 2016, Juin 2016, pp.6, Paris France, [ .pdf ]
Ce document décrit la conception, la reéalisation et l’expérimentation de «Danse-doigts», une application ludo-thérapeutique à destination d'enfants hémiparétiques. L'objectif de ce logiciel est double : permettre d'entraîner leur motricité fine sur tablette puis d'étudier l'effet de cet entraînement sur leurs compétences numériques (dénombrement, calcul,...). La population visée, comme l'objectif d'évaluation des compétences de calcul, ont influencé la conception. Le développement logiciel se base sur des technologies Web standard mais repose sur une bibliothèque de programmation parallèle en javascript. Applications et bibliothèques sont disponibles gratuitement et s'installent très facilement sur la plupart des tablettes tactiles.

[2] Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated certified proofs with cime3. In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs, pages 21--30. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. [ bib | DOI | http | .pdf ]
We present the rewriting toolkit CiME3. Amongst other original features, this version enjoys two kinds of engines: to handle and discover proofs of various properties of rewriting systems, and to generate Coq scripts from proof traces given in certification problem format in order to certify them with a sceptical proof assistant like Coq. Thus, these features open the way for using CiME3 to add automation to proofs of termination or confluence in a formal development in the Coq proof assistant.

[3] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated certified proofs with cime3. Technical Report 2044, CEDRIC laboratory, CNAM-Paris, France, Feb 2011. [ bib | .pdf ]
A preliminary version of [1].

[4] Pierre Courtieu, Gladys Gbedo, and Olivier Pons. Improved matrix interpretation. In Jan van Leeuwen, Anca Muscholl, David Peleg, Jaroslav Pokorný, and Bernhard Rumpe, editors, SOFSEM, volume 5901 of Lecture Notes in Computer Science, pages 283--295. Springer, 2010. [ bib | .pdf ]
We present a new technique to prove termination of Term Rewriting Systems, with full automation. A crucial task in this context is to find suitable well-founded orderings. A popular approach consists in interpreting terms into a domain equipped with an adequate well-founded ordering. In addition to the usual interpretations: natural numbers or polynomials over integer/rational numbers, the recently introduced matrix based interpretations have proved to be very efficient regarding termination of string rewriting and of term rewriting. In this spirit we propose to interpret terms as polynomials over integer matrices. Designed for term rewriting, our generalisation subsumes previous approaches allowing for more orderings without increasing the search space. Thus it performs better than the original version. Another advantage is that, interpreting terms to actual polynomials of matrices, it opens the way to matrix non linear interpretations. This result is implemented in the CiME3 rewriting toolkit

[5] Evelyne Contejean, Andrey Paskevich, Xavier Urbain, Pierre Courtieu, Olivier Pons, and Julien Forest. A3pat, an approach for certified automated termination proofs. In John P. Gallagher and Janis Voigtländer, editors, PEPM, pages 63--72. ACM, 2010. [ bib | .pdf ]
Software engineering, automated reasoning, rule-based programming or specifications often use rewriting systems for which termination, among other properties, may have to be ensured. This paper presents the approach developed in Project A3PAT to discover and moreover certify, with full automation, termination proofs for term rewriting systems.
It consists of two developments:the COCCINELLE library formalises numerous rewriting techniques and termination criteria for the COQ proof assistant; the CiME3 rewriting tool translates termination proofs (discovered by itself or other tools) into traces that are certified by COQ assisted by COCCINELLE.
The abstraction level of our formalisation allowed us to weaken premises of some theorems known in the literature, thus yielding new termination criteria, such as an extension of the powerful sub-term criterion (for which we propose the first full COQ formalisation). Techniques employed in CiME3 also improve on previous works on formalisation and analysis of dependency graphs.

[6] Pierre Courtieu, Gladys Gbedo, and Olivier Pons. Matrix interpretations revisited. In Alfons Geser and Johannes Waldmann, editors, Extended Abstracts of the 10th International Workshop on Termination, WST'09, Leipzig, Germany, page 4, Jun 2009. [ bib | .pdf ]

[6] Ivan Augé, Vincent Leligeour, and Olivier Pons. A distribution and system compiler for handling heterogeneous computer site. Technical Report 1549, CEDRIC laboratory, CNAM-Paris, France, 01 2008. [ bib | .pdf ]
This document describes YaKa, a complete solution for deploying operating systems on large computer site. Unlike most existing tools Yaka is based on a compiled approach. It provides a language allowing to describe a computer site as a whole and at all levels: host hardware, systems to install on the hosts, links between host systems, software generation. Using this description a compiler generates automatically the systems to be installed for each host and generates the network installation servers. All generated systems are ready to use and fully operational on their first run. All systems are generated in a single operation so every component is generated with a complete knowledge of all the other components of the system and a complete knowledge of the network relationship between the hosts. This ensures the coherence of each piece of software with the other softwares of the system and with the environment of the host. By reducing the amount of components needing to be installed and the complexity of the startup scripts, this drastically decreases the duration of system installation and the duration of the boot. This allows to do statically a lot of verifications. This allows to group tools together to provide abstract services. The power of the language is also demonstrated by describing a complete source based Linux distribution. The efficiency and reliability have been demonstrated by its use for several years to manage the teaching network our postgraduate school.(10 servers, 100 clients with heterogeneous hardware, different operating systems and software).

[8] Ivan Augé and Olivier Pons. A service oriented compiler for operating systems. Technical Report 1551, CEDRIC laboratory, CNAM-Paris, France, 01 2008. [ bib | .pdf ]
Most tools dedicated to system administration of local area network follow the same scheme. For each host they install an initial operating system and then update it using a package manager. The package managers run independently on the hosts, this makes difficult (even impossible) to create and maintain a stable environment in which multiple hosts coexist and cooperate. Furthermore, over time, the update process that upgrades, adds or suppress software results in instability of host systems. Finally, a package corresponds most often to a single software with a basic configuration which does not match to the network requirements. This article presents the YaKa framework which propose an orthogonal approach to this scheme in which the update feature almost disappears and is replaced by a very fast installation of a new clean system. All systems required in the network are generated all together by a compiler which has a complete view of the network. This general view allows to describe systems as a set of abstract services. A service groups one or several softwares and configures them for enabling a given functionality on one or several hosts.

[9] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. Rapport scientifique 1185, Cedric, 2007. [ bib | .pdf | .ps.gz ]
A preliminary version of [9].

[10] Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. In Boris Konev and Frank Wolter, editors, FroCos, volume 4720 of Lecture Notes in Computer Science, pages 148--162. Springer, 2007. [ bib | .pdf ]
Nowadays, formal methods rely on tools of different kinds: proof assistants with which the user interacts to discover a proof step by step; and fully automated tools which make use of (intricate) decision procedures. But while some proof assistants can check the soundness of a proof, they lack automation. Regarding automated tools, one still has to be satisfied with their answers Yes/No/Donotknow, the validity of which can be subject to question, in particular because of the increasing size and complexity of these tools. In the context of rewriting techniques, we aim at bridging the gap between proof assistants that yield formal guarantees of reliability and highly automated tools one has to trust. We present an approach making use of both shallow and deep embeddings. We illustrate this approach with a prototype based on the CiME rewriting toolbox, which can discover involved termination proofs that can be certified by the Coq proof assistant, using the Coccinelle library for rewriting.

[11] Brigitte Grau, Gabriel Illouz, Laura Monceaux, Patrick Paroubek, Olivier Pons, Isabelle Robba, and Anne Vilnat. Frasques, le système du groupe lir, limsi. In Atelier EQueR, Conférence (TALN'05), pages 85--88, June 2005. [ bib | .pdf | .ps.gz ]
Le système FRASQUES qui a participé à l'évaluation EQueR est présenté ici en comparaison avec le système QUALC dédié à l'anglais. Ses Résultats sont commentés en une évaluation des différents modules est exposée.

[12] Brigitte Grau, Anne-Laure Ligozat, Isabelle Robba, Anne Vilnat, Faîza El Kateb, Gabriel Illouz, Laura Monceaux, Patrick Paroubek, and Olivier Pons. De l'importance des synonymes pour la sélection de passages en question-réponse. In Conférence en Recherche d'Informations et Applications (CORIA'05), pages 71--84, March 2005. [ bib | .pdf | .ps.gz ]
Les systèmes de question-réponse développés actuellement adoptent pour la plupart et à peu de chose près le même type d'architecture que l'on peut schématiser en trois modules : l'analyse de la question, la sélection des documents, l'extraction de la réponse. Mais ce en quoi ils diffèrent, ce sont les outils (moteur d'indexation, analyseurs...) et les bases de connaissances qu'ils utilise nt. Pour chacun de ces systèmes, il est donc important d'évaluer l'apport de ces outils ou bases de connaissances. Dans le cadre de la campagne Equer (campagne d'évaluation des systèmes de question-réponse pour le français), notre système F RASQUES a produit deux jeux de résultats : l'un utilise des synonymes dans les b i-termes, l'autre pour les mono-termes aussi. La comparaison de ces deux tests e t l'étude d'un corpus plus large, en français et en anglais, permet de mesurer l'apport de ces connaissances sémantiques.

[13] Catherine Dubois, Mathieu Jaume, Olivier Pons, and Virgile Prevosto. L'atelier focal. In Actes du Congrès AFADL'04, Approches Formelles dans l'Assistance au Développement de Logiciels (Session Outils), Besancon, France, June 2004. [ bib | .pdf | .ps.gz ]
L'atelier FOCAL est un atelier intégré de construction modulaire de logiciels certifiés. Il permet l'écriture de modules constitués de déclarations, définitions, énoncés et preuves. Les déclarations peuvent être raffinées en définitions et les énoncés en preuves, par passage progressif de la spécification à l'implantation, à l'aide de mécanismes d'héritage, de redéfinition et d'instanciation de paramètres génériques. La compilation des modules développés avec l'atelier FOCAL produit un code exécutable OCaml et un développement formel Coq.

[14] Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory. Journal of Functional Programming, 13(2):261--293, 2003. [ bib | .pdf | .ps.gz ]
Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for developing mathematics. According to whether the equality relation is required to be reflexive or not we have total or partial setoid, respectively. There is only one definition of total setoid, but four different definitions of partial setoid, depending on four different notions of setoid function. We prove that one approach to partial setoids in unsuitable, and that the other approaches can be divided in two classes of equivalence. One class contains definitions of partial setoids that are equivalent to total setoids; the other class contains an inherently different definition, that has been useful in the modeling of type systems. We also provide some elements of discussion on the merits of each approach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty with the common definition of subsetoids in the partial setoid approach.

[15] Olivier Pons. Generalization in type theory based proof assistants. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, TYPES, volume 2277 of Lecture Notes in Computer Science, pages 217--232. Springer, December 2000. [ bib | .pdf | .ps.gz ]
This paper describes a mechanism to generalize mathematical results in type theory based proof assistants. The proposed mechanism starts from a proved theorem or a proved set of theorems (a theory) and makes it possible to get less specific results that can be instantiated and reused in other contexts.

[16] Gilles Barthe and Olivier Pons. Type isomorphisms and proof reuse in dependent type theory. In Furio Honsell and Marino Miculan, editors, FoSSaCS, volume 2030 of Lecture Notes in Computer Science, pages 57--71. Springer, 2001. [ bib | .pdf | .ps.gz ]
We propose a theoretical foundation for proof reuse, based on the novel idea of a computational interpretation of type isomorphisms.

[17] Yves Bertot, Olivier Pons, and Loïc Pottier. Graphes de dépendance pour les démonstrateurs de théorèmes intéractifs. Technical Report RR-4052, Institut National de Recherche en Informatique et en Automatique (INRIA), November 2000. [ bib | .pdf | .ps.gz ]
We propose tools to visualize large proof developments as graphs of theorems and definitions where edges denote the dependency between two theorems. In particular, we study means to limit the size of graphs. Experiments have been done with the Coq theorem prover and the GraphViz and daVinci graph visualization suites.
Keywords: Dependency, graphs, theorems, proof, Coq, GraphViz, daVinci, dot

[18] Olivier Pons. Proof engineering. Rapport de recherche, Laboratoire CEDRIC-CNRAM, September 2000. [ bib | .pdf | .ps.gz ]
The main purpose of this article is to present a panorama of tools for formal proof analysis and management. The proposed tools are based upon several notions of dependency. Our principal objective is to facilitate the development and the maintenance of theories in proofs assistants in order to improve the productivity of such systems' users.

[19] Olivier Pons. Proof generalization and proof reuse. Technical Report 2000 [ bib ]
This paper presents some experiments about the notion of generalization in proof assistants based on proof theory. We propose a mechanism which, starting from a proved theorem, allows to get a less specific result that can be instantiated and reused in other contexts.

[20] Olivier Pons. Ingénierie de preuve. In INRIA, editor, Actes des Journées francophones des langages applicatifs 2000, pages 171 -- 186, Mont Saint-Michel, France, January 2000. [ bib | .pdf | .ps.gz ]
This paper introduces a panorama of tools to analyse and to manage formal proofs. The goal of the proposed tools is to to facilitate the development and maintenance of theories in proof assistants and so to improve the productivity of the users of these systems.

[21] 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, Paris, France, July 1999. [ bib | .pdf | .ps.gz ]
Cette thèse s'inscrit dans un domaine de recherche dont l'objectif est le développement de systèmes interactifs d'aide à la démonstration, telque Coq, HOL ou PVS. Le but est de fournir des outils pour améliorer la productivité des utilisateurs de tels systèmes, lorsqu'ils sont engagés dans le développement de grandes théories mathématiques. Les outils proposés s'appliquent aux tâches de développement et de maintenance et sont basés sur différentes notions de dépendance.

Dans les assistants de preuve, l'utilisateur exprime sa démonstration sous la forme d'une suite de commandes (les tactiques). Chaque commande transforme un but en une liste de sous-buts plus simples à résoudre. Cette suite d'instructions peut être structurée sous forme d'un arbre de preuve qui reflète la structure logique de la preuve et les dépendances entre les différentes sous-preuves. Certains systèmes comme le système Coq utilisent également une notion d'objet preuve, représenté par exemple par un terme du lambda-calcul, qui fournit également de nombreuses informations utiles.

La première partie de cette thèse présente des outils permettant une "micro-assistance à l'utilisateur". On commence par présenter des outils de visualisation graphique de l'arbre de démonstration et de navigation dans la représentation textuelle de la preuve. On propose ensuite un mécanisme de retour-arrière logique qui permet de supprimer une commande du script de preuve sans affecter les parties de la preuve logiquement indépendantes de la tactique à supprimer. Il est apparu que cette indépendance elle-même n'est pas un simple reflet de la structure arborescente de l'arbre de démonstration, à cause de la présence de variables existentielles qui peuvent introduire des contraintes entre noeuds frères. Nous proposons des solutions pragmatiques pour préserver les avantages du retour-arrière logique en présence de variables existentielles. Le chapitre suivant présente des outils permettant d'agréger des commandes à l'aide de tacticielles ou au contraire de les développer en supprimant ces tacticielles. Ces outils d'expansion sont utilisés pour détecter des commandes inutiles, sécuriser le code, ou localiser des erreurs. Enfin, un dernier outil extrait un lemme d'une démonstration pour en faire un résultat à part entière.

D'autre part, dans les assistants de preuve, un développement est un ensemble de définitions et de théorèmes. Il est important d'essayer de regrouper entre elles les parties sémantiquement liées. Un tel regroupement forme alors une théorie. L'organisation des théories peut influencer de façon importante la vitesse de développement des preuves et leur réutilisabilité. La seconde partie de cette thèse, présente des outils fournissant une "macro-assistance" à l'utilisateur, c'est-à-dire une aide dans l'organisation des résultats en théories. L'outil de base dans cette partie est un programme d'analyse des dépendances entre les différents théorèmes qui constituent un développement. Le graphe de dépendance résultant est ensuite utilisé pour implanter différents outils. Là encore on commence par fournir des outils de visualisation. On propose ensuite une notion de coupe de théorie (inspirée de la notion de coupe de programme) qui consiste à supprimer d'un développement les résultats inutiles à l'établissement d'un théorème donné. L'outil suivant est le "reset logique" qui est l'analogue au niveau macroscopique du retour-arrière logique de la première partie. Enfin, on propose des outils pour réorganiser des résultats, par déplacement de code, ainsi que des outils fournissant une aide interactive à la propagation de modifications.

Dans un dernier chapitre, on aborde, essentiellement au travers d'exemples, différents moyens de fournir une aide à la généralisation de théori es.

Nous avons développé nos outils pour le système Coq, mais nous avons toujours tenté de définir des méthodologies génériques utilisables pour d'autres systèmes d'aide à la preuve (comme HOL, Lego ou PVS).

Enfin les outils présentés ne prennent leur pleine potentialité que dans cadre d'une interface graphique. Nos expériences ont été menées dans l'environnement CtCoq mais pourraient s'adapter à des environnements moins structurés comme l'environnement ProofGeneral basé sur Emacs.

[22] Olivier Pons, Yves Bertot, and Laurence Rideau. Notions of dependency in proof assistants. In Electronic Proceedings of "User Interfaces for Theorem Provers 1998", Sophia-Antipolis, France, July 1998. [ bib | .pdf | .ps.gz ]
This article describes uses of dependencies in tools to maintain big proofs in interactive proof assistants.

[23] Olivier Pons. Undoing and managing a proof. In Electronic Proceedings of "User Interfaces for Theorem Provers 1997", Sophia-Antipolis, France, September 1997. [ bib | .pdf | .ps.gz ]
In this paper we work in the area of proof script management. We study the dependencies between commands in a script and how they can be exploited in the undoing process. We present some problems that we have met in our implementation of proof managing tools in the CtCoq interface for the Coq System.

[24] Olivier Pons. Vers une formalisation de l'algèbre relationel en coq. Rapport de dea, Université Pierre et Marie Curie - Paris 6, Paris, France, September 1995. [ bib | .pdf | .ps.gz ]
C'est complètement dépassé et j'ai un peu honte mais ça peut remonter le moral de ceux qui ont du mal en MASTER!

[25] Ivan Augé and Olivier Pons. Fokon; un système d'éxamination automatique, 2008. [ bib | .pdf ]
Cet article décrit Fokon, un logiciel qui automatise entièrement la correction, la notation et l'établissement de rapports d'examen. Ce logiciel est utilisé en production à l'ENSIIE depuis 2005. Le cahier des charges qui a conduit à sa conception ainsi que le fonctionnement global et la méthode de notation sont tour a tour présentés.

[26] Pierre Courtieu and Olivier Pons. Formalisation d'un cours de logique et de sémantique en coq, 2014. [ bib | http ]

Quelques outils et logiciels

  • Danse-doigts, un jeu de motricité fine
  • CiME 3 et (et 2,99beta): une boite à outil de réécriture fondée sur CiME 2 et produisant des traces certifiables par des assistants de preuve.
    Dévellopé avec Évelyne Contejean, Pierre Courtieu, Julien Forest et Xavier Urbain. 52000 lignes de code OCAML
    Disponible à Licence CeCILL-C. (2007 -)
  • davinciML Une api ocaml pour le visualisateur de graphe uDraw
    Licence GNU (1998 -)
  • FoKon, un outil de correction et de notation automatique
    Dévellopé avec Ivan Augé. Licence GNU (2004).
    Je ne maintiens plus Fokon depuis mon dépard de l'IIE mais vous trouverez ici un miroir du site de l'époque (2007).
  • Deduction , un outil web graphique pour l'apprentissage de la déduction naturelle.
    Licence GNU (2007 - )