Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat de FILLIÂTRE Jean-Christophe
FILLIÂTRE Jean-Christophe
Doctorat
Equipe : Toccata

Preuve de programmes impératifs en théorie des types

Début le 01/09/1994
Direction : PAULIN-MOHRING, Christine

Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay

Lieu de déroulement :

Soutenue le 12/07/1999 devant le jury composé de :
M. Beauquier J.
Mme Viguié Donzeau-Gouge V.
M. Reynolds J. C.
M. Bidoit M.
M. Murthy C.
Mme Paulin C.

Activités de recherche :

Résumé :
Nous étudions le problème de la certification de programmes mêlant
traits impératifs et fonctionnels dans le cadre de la théorie des
types.

La théorie des types constitue un puissant langage de spécification,
naturellement adapté à la preuve de programmes purement fonctionnels.
Pour y certifier également des programmes impératifs, nous commençons
par exprimer leur sémantique de manière purement fonctionnelle. Cette
traduction repose sur une analyse statique des effets de bord des
programmes, et sur l'utilisation de la notion de monade, notion que
nous raffinons en l'associant à la notion d'effet de manière générale.
Nous montrons que cette traduction est sémantiquement correcte.

Puis, à partir d'un programme annoté, nous construisons une preuve de
sa spécification, traduite de manière fonctionnelle. Cette preuve est
bâtie sur la traduction fonctionnelle précédemment introduite. Elle
est presque toujours incomplète, les parties manquantes étant autant
d'obligations de preuve qui seront laissées à la charge de
l'utilisateur. Nous montrons que la validité de ces obligations
entraîne la correction totale du programme.

Nous avons implanté notre travail dans l'assistant de preuve Coq,
avec lequel il est dès à présent distribué. Cette implantation se
présente sous la forme d'une tactique prenant en argument un programme
annoté et engendrant les obligations de preuve. Plusieurs algorithmes
non triviaux ont été certifiés à l'aide de cet outil (Find, Quicksort,
Heapsort, algorithme de Knuth-Morris-Pratt).