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
0C8.

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.

Rapporteurs :

Mme. Catarina Coquand (rapporteur)
M. Christophe Raffalli (co-rapporteur)

Jury :

M. Guy Cousineau (président)
Mme. Catarina Coquand
M. Christophe Raffalli
M. Pascal Manoury
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