The goal of this internship is to show that the information that are in these proof terms can be used for other purposes. For this, we are going to concentrate on all the arithmetic statements that have been proved in Coq. Many contributions in the Coq libraries deal with arithmetic statements: they come from different developpers at different period of times. The idea is to build some tools to explore arithmetic proof terms in order to extract pertinent information that could be used for refactoring proof developments.
Requirements for this internship is an interesting in sofware engineering and functional programming.
Le but de ce stage est de montrer que les informations contenues dans ces objets preuve peuvent être utilisées à d'autres fins. Pour cela, nous nous concentrerons aux énoncés arithmétiques prouvés en Coq. Dans les contributions de Coq, il y a beaucoup de développements qui concernent l'arithmétique: ils proviennent de differents auteurs à différents époques. L'idée de ce stage est de construire des outils d'analyse des preuves des énoncés arithmétiques pour en extraire des informations pertinentes qui pourront ensuite être utilisés pour la réorganisation de développements formels.
Les prérequis pour ce stage sont un intérêt pour le génie logiciel et la programmation fonctionnelle.