Le projet Lemme s'intéresse au développement de programmes certifiés et efficaces. Pour cela, il utilise l'assistant de preuve Coq et un environnement de travail graphique qu'il développe, Pcoq.
Les scripts de preuves sont les documents manipulés par Pcoq. Ils contiennent la suite des commandes envoyées au programme Coq pour un développement particulier. Ces commandes sont simplement énumérées dans une longue liste d'opérations. Le but du stage et d'améliorer cette situation en transformant cette liste d'opérations en une structure plus arborescente, qui permet alors de mieux visualiser les commandes qui vont ensemble, de cacher des sections, etc. Le résultat obtenu devrait permettre de simuler les modes "plan" ou "outline" fournis par les éditeurs de documents grands publics.
L'outil pcoq est écrit en Java. Le stagiaire sera amené à travailler dans ce langage et à utiliser le format XML pour effectuer des sauvegardes structurées.
Yves Bertot
Yves.Bertot@sophia.inria.fr
tél: 04 92 38 77 39