Le système Coq comporte de longue date un outil d'extraction, permettant d'obtenir des programmes fonctionnels certifiés à partir de preuves constructives. Mais le mécanisme d'extraction précédent présentait d'importantes limitations. Certaines preuves Coq étaient ainsi hors de son champ d'application, alors que d'autres pouvaient mener à des programmes incorrects.
Afin de résoudre ces limitations, j'ai effectué au cours de ma thèse au LRI une refonte complète de l'extraction Coq, tant du point de vue de la théorie que de l'implantation. Au niveau théorique, cette refonte a entraîné la réalisation de nouvelles preuves de correction de ce mécanisme d'extraction. La bonne réduction des programmes extraits est prouvée par des moyens syntaxiques, à savoir une bisimulation avec les réductions Coq. En outre, pour garantir la correction syntaxique de l'extraction, une relation de réalisabilité a finalement pu être mise au point.
Concernant l'implantation, je me suis efforcé d'engendrer du code extrait efficace et réaliste, pouvant en particulier être intégré dans des développements logiciels de plus grande échelle, par le biais de modules et d'interfaces. Plusieurs études de cas ont permis de vérifier les progrès accomplis.