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.

We present a formal proof (at the implementation level) of an efficient algorithm proposed by Paul Zimmermann to compute square roots of arbitrarily large integers. This program, which is part of the GNU Multiple Precision Arithmetic Library (GMP), is completely proven within the Coq system. Proofs are developed using the Correctness tool to deal with imperative features of the program. The formalization is rather large (more than 13000 lines) and requires some advanced techniques for proof management and reuse.

In a theorem prover like Coq, mathematical concepts can be implemented in several ways. Their different representations can be either efficient for computing or well-suited to carry out proofs easily. In this paper, we present improved techniques to deal with changes of data representation within Coq. We propose a smart handling of case analysis and definitions together with some general methods to transfer recursion operators and their reduction rules from one setting to another. Once we have built a formal correspondence between two settings, we can translate automatically properties obtained in the initial setting into new properties in the target setting. We successfully experiment with changing Peano's numbers into binary numbers for the whole Arith library of Coq as well as with changing polymorphic lists into reversed (snoc) lists.

In type-theory based proof systems that provide inductive structures, computation tools are automatically associated to inductive definitions. Choosing a particular representation for a given concept has a strong influence on proof structure. We propose a method to make the change from one representation to another easier, by systematically translating proofs from one context to another. We show how this method works by using it on natural numbers, for which a unary representation (based on Peano axioms) and a binary representation are available. This method leads to an automatic translation tool that we have implemented in Coq and successfully applied to several arithmetical theorems.

Dans le calcul des constructions inductives, des outils de calcul et de preuve sont associés à chaque type de données concret défini inductivement. Par conséquent, le choix d'une structure de données influence fortement le contenu des preuves. Nous proposons dans ce document une méthode pour passer facilement d'une représentation à une autre, en effectuant des traductions partiellement automatisées des preuves. Nous mettons cette méthode en oeuvre sur les entiers naturels, pour lesquels il existe une représentation unaire (à la Peano) et une représentation binaire. Un prototype d'outil de traduction est développé dans le système Coq et a été expérimenté avec succès sur une dizaine de théorèmes d'arithmétique.

We present the formal proofs of total correctness of three sorting algorithms in the Coq system, namely insertion sort, quicksort and heapsort. The implementations are imperative programs working in-place on a given array. Those developments demonstrate the usefulness of inductive types and higher-order logic in the process of software certification. They also show that the proof of rather complex algorithms may be done in a small amount of time - only a few days for each development - and without great difficulty.