Insertion dans la communauté scientifique

Thématiquement, notre projet est naturellement lié à trois domaines : les environnements de certification de programmes, la théorie des types et le calcul formel.

Collaborations effectives

A l'INRIA

• COQ : Le projet Coq est évidemment une des équipes avec laquelle nous collaborons et avec qui nous collaborerons le plus. D'abord parce que pratiquement, nos travaux serons exprimés dans le CCI et testés sur le système Coq, via l'interface CtCoq développée par CROAP depuis 4 ans, ensuite parce le projet Coq, depuis sa création, a, à la base de ses réflexions, le problème de la formalisation des mathématiques. Le calcul scientifique y a aussi une place, avec les travaux de Benjamin Werner sur l'algorithme de Buchberger, ceux de Micaela Mayero sur l'analyse réelle. Coq fait aussi partie, comme feu-CROAP, de l'action coopérative ``Calcul Formel Certifié'', et c'est dans ce cadre par exemple que l'extraction a été étendue à tout le CCI.

• CODES : en codage et en cryptographie, la sûreté des implantations est critique. Extraire du code C d'algorithmes prouvés semble une voie vers des applications concrètes de nos travaux, que nous explorons en ce moment avec Daniel Augot. Pratiquement cela conduit à un travail qui commence sur RSA avec Gilles Barthe, et à un sujet de stage sur la certification de PGP [2].

• CFC :

  Nous avons un rôle moteur dans l'action coopérative ``Calcul formel certifié'', qui regroupe les équipes Calfor (Daniel Lazard), SPI (Thérèse Hardin), ainsi que les projets Coq et Cristal. Le but de cette action est mener des recherches pour obtenir des implantations d'algorithmes de calcul formel qui soient efficaces et formellement certifiées. Pratiquement, un noyau de système de calcul formel centré sur l'algèbre commutative est développé en Ocaml dans le projet FOC (Calfor+SPI). De notre côté, nous développons en Coq une bibliothèque de théories mathématiques correspondantes (structures et propriétés). Le lien entre ces deux développements étant d'une part étudié via une extension de l'extraction de Coq vers Ocaml (classes et modules), et d'autre part un langage (FOC) utilisateur donnant accès aux deux mondes Coq et Ocaml [1].

  Les algorithmes en point de mire dans CFC sont l'algorithme des sous-résultants (Sylvain Boulmé), les calculs sur les nombres algébriques réels (Renaud Rioboo), et RSA (Gilles Barthe).

Cornell, USA

Yves Bertot vient de passer deux semaines dans l'équipe du professeur Constable à l'université de Cornell. Cette équipe étudie depuis longtemps un éventail de problèmes proches de ceux abordés par notre équipe et l'équipe Coq. Parmi les points plus spécifiquement reliés à nos objectifs, nous devons citer leur effort de développement pour fournir une interface homme-machine multi-fenêtre, orientée vers la manipulation structurée des formules mathématiques, une étude approfondie de l'extraction de programmes et des tentatives pour intégrer calcul algébrique et déduction. Il faut noter que NuPrl est utilisé avec succès dans la vérification formelle de logiciels de travail collaboratif sur réseau : le système Ensemble proposé par l'équipe de Ken. Birman.

Le système formel fourni par NuPrl est par certains égards moins efficace mais plus puissant que celui fourni par Coq. La différence réside en le fait que le système formel des constructions inductives de Coq est plus contraint : intuitivement, Coq permet de travailler sur des programmes fortement typés similaires à ce que l'on écrit en ML, tandis que NuPrl permet de raisonner sur des programmes faiblement typés comme ceux que l'on écrit en Lisp. Les contraintes apportées en Coq permettent de se restreindre à un domaine pour lequel les techniques de preuves peuvent être optimisées et la compilation peut être très efficace, grâce en particulier au compilateur Ocaml. En revanche, le système NuPrl permet de raisonner sur des algorithmes que l'on ne sait pas décrire en Coq.

Dans le domaine des interfaces homme-machine, l'expérience de NuPrl est difficile à apprécier. Leurs travaux fourmillent d'idées originales et productives, mais le manque d'uniformité fait que l'interface homme-machine de NuPrl est peut-être le principal obstacle à la diffusion du système de preuve.

Types

Le groupe de travail européen Types sous ses diverses incarnations (Working Group, Basic Research Action, ...) est le lieu de rencontres des équipes européennes intéressées par la théorie des types. Le groupe de travail actuel `Types and Programms' dont fait partie CROAP se termine courant 1999. Lemme participera à l'élaboration des propositions de renouvellement de ce groupe de travail.

Calculemus

Le groupe de travail Calculemus a une thématique très proche de Lemme puisqu'il se propose d'unifier les efforts de trois communautés (celles du calcul formel, des démonstrateurs interactifs et des preuves automatiques). Depuis le début, les membres de l'équipe Lemme ont participé aux différentes réunions de ce groupe de travail. Nijmegen, Eindhoven et Risc font aussi partie de ce groupe de travail.

UITP (User-Interfaces for Theorem Provers)

Nous participons depuis sa création au cycle de colloques UITP où nous rencontrons la majeure partie des équipes dans le monde qui s'intéressent à ce domaine. Les objectifs des différentes équipes varient de l'outil de preuve pour l'enseignement de la logique à l'outil de démonstration automatique dans un thème particulier, en passant par l'étude générale de l'ergonomie des interfaces et les outils d'édition de documents mathématiques. Nos compétences dans ce forum sont reconnues, puisque nous avons été invités à plusieurs reprises dans le comité de programme et nous avons organisé l'édition 1997.

Calcul formel

Les méthodes formelles sont actuellement quasi-absentes de la communauté du calcul formel. On espère que des implantations certifiées et efficaces d'algorithmes de calcul formel pourront avoir une utilité dans les systèmes de calcul formel. Nous avons eu des échos favorables, par exemple lors de la présentation de Gbcoq (implantation certifiée de calculs de bases de Groner) à MEGA'98.

Collaborations à développer et contexte

A l'INRIA

• ALGO : spécialiste du calcul formel, de Maple, le projet ALGO nous a déjà donné du grain à moudre, par exemple avec la preuve en Coq de l'algorithme de factorisation dans les corps finis de Cantor-Zassenhaus, pour laquelle nous nous sommes fondés sur les travaux du projet [22]. Si extraire du code Maple a un sens pratique, c'est par exemple avec ALGO que ce travail peut se faire.

• POLKA, SAGA, PRISME, CAFÉ : spécialistes d'algorithmiques variés, gros utilisateurs et développeurs de mathématiques et de calcul formel, ces projets sont pour nous une source d'inspiration et d'expérimentations. Nous serions heureux de faire notre marché dans leur stock d'algorithmes !

• MEIJE : dans la branche de ce projet qui se concentre sur Esterel, le problème de vérifier les algorithmes fondamentaux du compilateur a déjà été abordé à l'aide de Coq et CtCoq par Delphine Terrasse. Ce projet est donc un utilisateur potentiel de nos outils et nous suivrons avec attention leurs travaux dans ce cadre.

• Action coopérative FIABLE : L'action coopérative FIABLE met l'accent sur le contrôle des erreurs, des spécifications, des algorithmes et de leur efficacité dans les calculs numériques (jusqu'au plus bas niveau). Nous devrions pouvoir montrer l'intérêt de la certification d'algorithmiques dans ce cadre, en prouvant puis extrayant en C des fragments d'arithmétique flottante ou entière vérifiant par exemple le norme ANSI/IEEE 754 sur les erreurs d'arrondis (déjà formalisée en Coq par Patrick Loiseleur).

• PROTHEO : fondé sur la réécriture, et spécialiste des preuves automatiques par récurrence. Le prouveur Spike peut donner lieu à une tactique Coq spécialisée pour les réécritures et les inductions complexes, comme il peut y en avoir en algorithmique.

• CRISTAL : pour l'extraction, on a besoin d'un évaluateur de $\lambda$-calcul pur avec pattern matching et récurseurs, ce qui pourrait se trouver avec Ocaml sans son typage. On pourrait aussi réfléchir avec les membres de Cristal et ceux de Coq sur un compilateur dédié à Coq et au CCI.

• CALLIGRAMME : groupant des spécialistes de la logique linéaire, du $\lambda$-calcul, et de linguistique, ce projet pourrait peut-être nous fournir des pistes pour la traduction textuelle de preuves ou d'énoncés mathématiques.

• COMPOSE : l'évaluation partielle et l'interprétation abstraite sont des techniques qui peuvent nous intéresser. Elles ne constitueront cependant pas une de nos priorités immédiates.

• PARA : Parmi les travaux effectués ces dernières années dans cette équipe, on peut citer la vérification formelle d'un algorithme de récupération de mémoire (Garbage Collection) en utilisant le système de preuve Larch. Ce projet dispose donc de compétences dans la vérification mécanique d'algorithmes qui sont complémentaires des nôtres.

Université Chalmers à Göteborg, Suède

T. Coquand et H. Person étudient la représentation des bases de Gröbner en théorie des types d'un point de vue constructif. Cela a conduit à une preuve constructive essentiellement nouvelle du théorème de la base de Hilbert. Un algorithme peut en être théoriquement extrait, dont la complexité est encore inconnue, mais qui n'est pas a priori du type Buchberger. Ces travaux sont à rapprocher de la preuve de l'algorithme de Buchberger de Laurent Théry, et du lemme de Dickson de Loïc Pottier. C'est clairement une équipe avec laquelle nous continuerons d'avoir des réflexions.

Université d'Eindhoven, Hollande

L'équipe de calcul formel d'Arjeh Cohen a un rôle important dans le projet Openmath (communication entre systèmes de calcul formel, Web), et étudie l'intérêt que pourrait apporter la théorie des types dans la nécessaire utilisation d'un langage commun pour représenter les objets mathématiques migrant d'un logiciel de calcul formel à l'autre. Nous sommes convaincus que c'est une très bonne voie, et comptons collaborer avec Arjeh Cohen et Olga Caprotti sur ce thème, sur la base de notre expérience de la formalisation de l'algèbre et des polynômes en Coq.

Université de Cambridge, GB

L'équipe du professeur Mike Gordon à Cambridge développe le démonstrateur HOL. L'intérêt de l'équipe se concentre principalement autour de la preuve de circuits intégrés. Dans ce cadre, un important travail a été réalisé par John Harrison [24] sur une formalisation des réels. Une des motivations de ce travail était de fournir les éléments pour vérifier les parties du microprocesseur qui se chargent des opérations arithmétiques flottantes. Le récent problème du Pentium a renforcé l'intérêt industriel pour une telle approche. Nous avons déjà collaboré avec cette équipe avec la construction d'une interface pour leur démonstrateur [43].

L'université de Cambridge est aussi le site où est développé le système de preuve Isabelle [36], en collaboration avec l'université de Munich. Isabelle est un système de preuve plus général que HOL plus orienté vers l'automatisation des preuves, en particulier avec une utilisation centrale de l'unification d'ordre supérieur. Ce système fait aussi l'objet d'efforts pour attacher une interface graphique puissante au système de preuve. En particulier, une équipe australienne avec laquelle nous avons des contacts réguliers développe Xisabelle [33].

Université de Nijmegen, Hollande

L'équipe de théorie des types de H. Barendregt étudie les preuves en calcul formel sous au moins deux aspects :

• en prouvant par exemple la primalité d'un entier, à partir d'un algorithme donnant un test de primalité. L'algorithme n'est pas à proprement parler prouvé : son exécution dans un cas particulier produit à la volée une preuve du résultat. Ceci s'apparente donc plutôt à une tactique particulière.

• en améliorant l'efficacité des calculs par une technique de réflexion dans le cas des fonctions primitives récursives.

Université de Berkeley, USA

Richard Fateman étudie de façon générale la numérisation de textes mathématiques, ainsi que leur utilisation interactive. Il a développé un prototype de reconnaissance de caractères et de formules mathématiques [5]. Avec la nôtre (Stéphane Lavirotte, Loïc Pottier), son équipe est une des rares qui travaille concrètement sur le sujet (une au Japon, une au Canada, une autre aux EUA).

Mizar, Pologne

Le but du projet Mizar est de fournir un support logiciel pour la publication de documents mathématiques. Les textes écrits en Mizar sont appelés articles et sont organisés en base de données. À ce jour cette base comporte plus de 500 articles. Elle représente un des plus importants efforts de formalisation des mathématiques sur machine. Mizar est fondé sur la théorie des ensembles de Tarski-Grothendieck. Une fois un article écrit, il est possible d'appliquer une procédure qui vérifie la consistance logique et la correction des références. Le projet Mizar est une source d'inspiration pour la diversité des théories mathématiques formalisées et pour le langage de spécification qu'ils ont élaboré qui se veut très proche du langage mathématique usuel.

Université d'Edinbourg, Écosse

L'équipe de R. Burstall à Edinbourg développe l'assistant de preuve Lego. Nous avons collaboré avec cette équipe sur le thème des environnements de démonstration, ce qui a mené à l'implantation de l'algorithme de preuve par sélection dans leur environnement de travail, fondé sur Emacs [12].

MathML

Le groupe de travail MathML propose un standard de communication des mathématiques sur l'internet utilisant XML. Un premier objectif de Lemme est d'évaluer la faisabilité de nous conformer à un tel standard dans le cadre des environnements de preuve.

Risc Linz, Autriche

L'équipe de Bruno Buchberger développe le système Theorema [17], visant à construire un environnement mêlant calcul formel et démonstrations mathématiques. Son approche est inverse de la nôtre. Il part du système de calcul formel Mathematica pour lui ajouter un moteur de preuve, et un environnement adapté.