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.