The Coq mailing list

[SB <Sylvain.Baro AT pps.jussieu.fr>]

J'ai le plaisir de vous inviter à ma soutenance de thèse ainsi -- bien
sûr -- qu'au traditionnel pot qui suivra.

La soutenance aura lieu le 10 juillet 2003 à 14h30 à Chevaleret, salle
0C6.

175 Rue du Chevaleret
75013 PARIS

Métro : Chevaleret ou Bibliothèque.

Ma thèse a pour titre :

                  Conception et implémentation d'un
                  système d'aide à la spécification
                   et à la preuve de programmes ML

et a été effectuée sous la direction de Pascal Manoury.

Les membres du jury sont :

M. Guy Cousineau (président)
Mme. Catarina Coquand (rapporteur)
M. René David (rapporteur)
M. Christophe Raffalli (co-rapporteur)
M. Pascal Manoury (directeur de thèse)
Mme. Véronique Donzeau-Gouge
M. Hugo Herbelin


Résumé (english abstract follows) :

Pouvoir vérifier la conformité d'un programme par rapport à sa
spécification représente un enjeu important. Pouvoir le faire à l'aide
d'une machine offre en plus la possibilité de << vérifier cette
vérification >>. On utilise pour cela un assistant de preuve
permettant la description du problème, la construction des preuves et
leur vérification.

Plusieurs approches existent pour parvenir à cette fin: engendrer le
programme à partir de sa spécification; utiliser un programme annoté
avec sa spécification et des éléments de preuves pour construire la
preuve complète de correction; ou encore partir de la spécification et
du programme, puis montrer la conformité du second vis-à-vis du
premier. C'est cette dernière approche que nous avons choisi.

Dans le système que nous avons implémenté, l'utilisateur décrit la
spécification du programme dans un formalisme logique ad hoc, puis
donne le programme dans le sous-ensemble fonctionnel de ML (comprenant
filtrage, définitions récursives et fonctions partielles), puis
construit interactivement les preuves de correction nécessaires pour
prouver la validité du programme.

Le travail que nous avons fourni se découpe en trois volets:
 -  la formalisation d'une logique dédiée à la preuve de
    programmes dans le fragment fonctionnel de ML;
 -  la spécification détaillée du moteur de preuve, de son
  interface, et du protocole qu'ils utilisent pour communiquer;
 - l'implémentation du moteur de preuve en Objective Caml, qui utilise
   une architecture particulièrement originale, mélangeant
   programmation objet et programmation fonctionnelle.


Tous ces éléments seront présentés, y compris une description de
l'implémentation, et des raisons qui nous ont poussés à effectuer
certains choix, plutôt que d'autres.


Abstract:

One should not underestimate the import of being able to verify the
conformance between a program and its specification. Furthermore,
being able to verify it using a dedicated program allows one to check
the correctness of this verification. For this purpose, one uses proof
assistants, which are programs that allows to describe the problem,
build proofs, then check them.

There are more than one way to achieve this goal: one could either
generate the program from its specification; one could use an
annotated program which carries the specification and hints on how to
prove the conformance, then check it afterwards; or one could start
from the specification and the program, then prove the conformance
of the latter with respect to the first. For our system, we chose
the last approach.

We implemented a system in which the user describes the specification
of a program in a dedicated logical framework, then writes the program
in the ML programming language, restricted to the  functional
subset (with pattern matching, inductive definitions and partial
functions), then, after all, interactively builds the proof of
conformance of the program with respect to its specification.

There are three different aspects in our work:
 - formalization of a logical framework dedicated to the
   verification of programs written in the functional part of ML;
 -  precize specification of the proof assistant, its user
interface, and the protocol used by both in order to communicate;
 - the implementation of the proof assistant in Objective Caml, using
   an original architecture which mixes object oriented programming
   and functional programming.

All these elements will be discuss, including a precize
description of the implementation, the choices we made and the reasons
of these choices.


-- 
                        |o|o|o|o      Sylvain Baro      |o|o|o|o

                                
Sylvain.Baro AT pps.jussieu.fr