The Coq mailing list

[Nicolas Magaud <Nicolas.Magaud AT sophia.inria.fr>]

Bonjour,

J'ai le plaisir de vous annoncer la soutenance prochaine de 
ma thèse, intitulée "Changements de Représentation des Données 
dans le Calcul des Constructions".

Cette soutenance aura lieu dans l'amphi Ouest de l'ESSI 
à Sophia-Antipolis le mardi 21 octobre 2003 à 14 heures.

Vous êtes tous invités à l'exposé ainsi qu'au pot qui le suivra.

-------------------------------------------------------------------------------
------
Titre : Changements de Représentation des Données dans le Calcul des 
Constructions

Résumé :
Nous étudions comment faciliter la réutilisation des preuves 
formelles en théorie des types. Nous traitons cette question 
lors de l'étude de la correction du programme de calcul de 
la racine carrée de GMP. A partir d'une description formelle, 
nous construisons un programme impératif avec l'outil Correctness.
Cette description prend en compte tous les détails de l'implantation,
y compris l'arithmétique de pointeurs utilisée et la gestion de la 
mémoire. Nous étudions aussi comment réutiliser des preuves formelles 
lorsque l'on change la représentation concrète des données. 
Nous proposons un outil qui permet d'abstraire les propriétés 
calculatoires associées à un type inductif dans les termes de preuve.
Nous proposons également des outils pour simuler ces propriétés
dans un type isomorphe. Nous pouvons ainsi passer, systématiquement,
d'une représentation des données à une autre dans un développement
formel.  

Abstract:
We study proof reuse in a type theory.
We investigate this issue by studying the correctness of GMP 
square root.  From a formal description, we
build a complete imperative program using the Correctness tool.  This
description gives a detailed account of the actual implementation,
including pointer arithmetics and memory management. 
We also study how to reuse formal proofs when the concrete representation of
some data changes.  We propose  tools to abstract away computational
properties of a given inductive data type in proof terms. We also propose 
new tools to simulate these properties in an isomorphic data type.
Together, these tools allow us to shift, almost automatically, from
one representation to another in a formal development.  

--
Nicolas Magaud                                 
mailto:nmagaud AT sophia.inria.fr
INRIA Sophia Antipolis - Projet Lemme         2004, route des Lucioles, BP 93
06902 Sophia Antipolis Cedex - FRANCE                tel:(+33/0)4 92 38 79 76
web:http://www-sop.inria.fr/lemme/Nicolas.Magaud