Programmation fonctionnelle certifiée : L'extraction de programmes dans l'assistant Coq

This work concerns the generation of programs which are certifiedto be correct by construction. These programs are obtained by extracting relevant information from constructive proofs made withthe Coq proof assistant. Such a translation, named ``extraction'', of constructive proofs intofunctional programs is not new, and corresponds to an isomorphismknown as Curry-Howard's. An extraction tool has been part of Coqassistant for a long time. But this old extraction tool suffered fromseveral limitations: in particular, some Coq proofs were refused byit, whereas some others led to incorrect programs.In order to overcome these limitations, we built a completely newextraction tool for Coq, including both a new theory and a newimplementation. Concerning theory, we developed new correctnessproofs for this extraction mechanism. These new proofs are both complex and original. Concerning implementation, we focused on the generation of efficient and realistic code, which can be integrated in large-scale software developments, using modules and interfaces.Finally, we also present several case studies illustrating thecapabilities of our new extraction. For example, we describe thecertification of a modular library of finite set structures, and the production of programs about real exact arithmetic, starting from aformalization of constructive real analysis. These examples show the progress already achieved, even if the situation is not perfect yet,in particular in the last study.; Nous nous intéressons ici à la génération de programmes certifiéscorrects par construction. Ces programmes sont obtenus enextrayant l'information pertinente de preuves constructives réaliséesdans l'assistant de preuves Coq.Une telle traduction, ou "extraction", des preuves constructivesen programmes fonctionnels n'est pas nouvelle, elle correspond à un isomorphisme bien connu sous le nom de Curry-Howard. Etl'assistant Coq comporte depuis longtemps un tel outil d'extraction. Mais l'outil précédent présentait d'importantes limitations. Certaines preuves Coq étaient ainsi hors de son champ d'application, alors que d'autres engendraient des programmes incorrects.Afin de résoudre ces limitations, nous avons effectué une refontecomplète de l'extraction dans Coq, tant du point de vue de la théorieque de l'implantation. Au niveau théorique, cette refonte a entraînéla réalisation de nouvelles preuves de correction de ce mécanismed'extraction, preuves à la fois complexes et originales. Concernantl'implantation, nous nous sommes efforcés d'engendrer du code extrait efficace et réaliste, pouvant en particulier être intégré dans desdéveloppement logiciels de plus grande échelle, par le biais demodules et d'interfaces.Enfin, nous présentons également plusieurs études de cas illustrantles possibilités de notre nouvelle extraction. Nous décrivons ainsi lacertification d'une bibliothèque modulaire d'ensembles finis, et l'obtention de programmes d'arithmétique réelle exacte à partir d'une formalisation d'analyse réelle constructive. Même si des progrès restent encore à obtenir, surtout dans ce dernier cas, ces exemples mettent en évidence le chemin déjà parcouru.