Changements de représentation des données dans le calcul des constructions
Institution:
NiceDisciplines:
Directors:
Abstract EN:
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.
Abstract FR:
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.