Conception et implantation du langage FoC pour le développement de logiciels certifiés

Cette these porte sur la construction d'un environnement pour developper des librairies de calcul formel certifie. Nous presentons d'abord les especes, structures servant a decrire des specifications par heritage multiple, raffinement et parametrisation. Les collections, construites par encapsulation d'especes constituent la librairie utilisateur. Nous definissons egalement les analyses statiques garantissant la correction d'une definition d'espece. Ensuite, nous etudions la compilation des especes et collections vers le langage d'execution OCAML, en utilisant les objets et modules OCAML. Puis nous detaillons la traduction dans le langage de preuves COQ, la liaison retardee etant traduite par des lambda-abstractions. Nous montrons ensuite comment utiliser cette technique pour optimiser les executables OCAML. Enfin, nous prouvons que les analyses faites par le compilateur ainsi que les techniques de traduction sont conforme a la formalisation des especes faites auparavant en COQ.