LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » News » PhD students

PRÉVOSTO Virgile

PhD graduated - SPI
Departure date : 10/17/2003
http://www-spi.lip6.fr/~prevosto/
Supervision : Thérèse HARDIN

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

Cette thèse porte sur la construction d'un environnement pour développer des librairies de calcul formel certifié. Nous présentons d'abord les espèces, structures servant à décrire des spécifications par héritage multiple, raffinement et paramétrisation. Les collections, construites par encapsulation d'espèces constituent la librairie utilisateur. Nous définissons également les analyses statiques garantissant la correction d'une définition d'espèce. Ensuite, nous étudions la compilation des espèces et collections vers le langage d'exécution OCAML, en utilisant les objets et modules OCAML. Puis nous détaillons la traduction dans le langage de preuves COQ, la liaison retardée étant traduite par des lambda-abstractions. Nous montrons ensuite comment utiliser cette technique pour optimiser les exécutables OCAML. Enfin, nous prouvons que les analyses faites par le compilateur ainsi que les techniques de traduction sont conforme à la formalisation des espèces faites auparavant en COQ.
Defence : 09/15/2003 - 14h - Site Scott - Salle Gérard Noguez
Jury members :
Christian QUEINNEC (président)
Claude KIRCHNER (rapporteur)
César MUÑOZ (rapporteur)
Gérard HUET (examinateur)
Damien DOLIGEZ (directeur)
Thérèse HARDIN (directrice)
Sylvain BOULMÉ (membre invité)

2001-2005 Publications

 Mentions légales
Site map |