Abstract FR:

Cette these decrit un systeme pour specifier, programmer et certifier (prouver) des bibliotheques de calcul formel. Chaque unite de bibliotheque represente une certaine structure algebrique, comme les groupes, les anneaux, les algebres de polynomes, etc. En pratique, les bibliotheques de calcul formel comportent un grand nombre de structures algebriques qui partagent entre elles algorithmes, proprietes et preuves, de facon assez compliquee. Par exemple, une notion calculatoire d'algebre (comme le pgcd) est definie par des proprietes algebriques. Toutes les structures algebriques verifiant ces proprietes partagent cette notion. Mais chacune d'elles peut l'implanter en utilisant differents algorithmes : generiques (communs a une large gamme de structures), ou specialises (utilisant une representation particuliere des donnees, ou communs a des structures verifiant une certaine propriete). Pour exprimer ce partage entre unites, l'utilisateur dispose de mecanismes d'heritage. L'heritage permet de creer une unite a partir de une ou plusieurs autres, en decrivant uniquement les differences de l'unite creee vis-a-vis des unites heritees, tout en preservant leurs proprietes. En effet, les algorithmes (et les preuves) applicables a une unite a seront aussi applicables a une unite b qui herite de a. Par rapport aux mecanismes traditionnels de programmation orientee objet, l'heritage est ici tres restreint de maniere a garantir la coherence logique des bibliotheques et la terminaison des programmes. Ce systeme est d'abord implante en coq. Il est ensuite decrit de maniere abstraite (independament de toute syntaxe), dans un metalangage categorique, en s'inspirant des categories contextuelles introduites par cartmell pour modeliser les types dependants. Pour donner lieu a des programmes executable, il est aussi propose une traduction de ces bibliotheques dans le langage ocaml, en utilisant divers traits de ce langage : polymorphisme, objets, modules, etc.