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.

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.

A preliminary version of [1].

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

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.

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).

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.

A preliminary version of [9].

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.

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.

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.

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.

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.

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.

We propose a theoretical foundation for proof reuse, based on the novel idea of a computational interpretation of type isomorphisms.

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

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.

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.

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.

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.

This article describes uses of dependencies in tools to maintain big proofs in interactive proof assistants.

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.

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!

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.