Objectifs à 3 ans

De manière un peu lapidaire, on peut dire que l'objectif de Lemme à l'horizon 2002 est la réalisation d'un environnement permettant le développement de programmes de calcul scientifiques certifiés, accessible à un public ignorant les méthodes formelles: ingénieurs, chercheurs, enseignants et étudiants.

Cet objectif implique des travaux de recherche et de développement, allant de pair avec des expérimentations dans différents domaines (industrie, enseignement), qui sont autant d'objectifs secondaires.

• Objectifs de recherche:

  Nous cherchons à comprendre et résoudre les problèmes suivants:

  • nouveaux moyens d'interaction dans les environnement d'aide à la preuve.

  • maintenance et utilisation de gros développements logiques.

  • méthodes pour l'algorithmique certifiée et efficace:

    • la récursion bien fondée comme technique de base (avec la récursion structurelle) dans l'écriture d'algorithmes en Coq.

    • gestion sûre et efficace de la mémoire (tableaux et pointeurs).

    • prouver la complexité d'un algorithme.

    • extraire tous les objets du calcul des constructions inductives dans des langages usuels (ocaml Java, C).

  • isoler des constructions élémentaires simples et puissantes pour la formalisation des mathématiques classiques dans le calcul des constructions inductives.

• Objectifs de développement:
  • à partir de CtCoq et Aïoli, réalisation d'une version ``grand public'' de Pcoq, diffusée sur internet ou par des CD-Rom, comme un outil interactif de développement mathématique portable sous Unix et Windows.

  • disposer dans Pcoq d'une version plus performante et extensible des outils de preuve à la souris et de présentation textuelle des preuves.

  • formaliser en Coq les mathématiques du premier cycle, et d'autres mathématiques plus savantes comme la géométrie algébrique, la théorie des groupes.

  • dans la veine de ce que l'on fait depuis deux ans, certifier des algorithmes de base du calcul scientifique: développements limités et calculs approchés, algorithmes cryptographiques.

  • développer, en collaboration avec des enseignants et sur la base des logiciels Pcoq et Wims, un logiciel d'aide à l'enseignement des mathématiques élémentaires. Ce développement sera utilisable via le Web comme un cours avec exercices interactifs.

• Expériences et applications:
  • Collaborer avec des industriels utilisant des méthodes formelles dans leurs développements logiciels (Coq, mais pas uniquement).

  • Diffuser Pcoq afin qu'il soit utilisé comme interface à Coq par une proportion non négligeable des utilisateurs de Coq.
  • Développer une expérience d'utilisation industrielle d'algorithmes de calcul scientifique certifiés.

  • Utiliser dans l'enseignement (université et écoles d'ingénieurs, en particulier à Nice et Sophia) l'association Pcoq+Wims.