Extraction de programmes plus efficaces à partir de preuves (non-constructives) par l'interprétation Dialectica Légère (Monotone).

This thesis presents a new optimization of Gödel's Dialectica interpretation for the extraction of more efficient exact realizers from (classical) arithmetical and even analytical proofs. The "light" variant of Dialectica also combines and even more smoothly with Kohlenbach's "monotone" optimization of Gödel's functional interpretation for the extraction of more efficient majorants and bounds from (classical)monotonic proofs. Light Dialectica is obtained by adapting Berger's "uniform" or "non-computational" quantifiers. Moreover, its presentation is given in Natural Deduction style, as an improvement of Jørgensen's recent adaptation of pure Gödel's Dialectica. A number of concrete examples are treated on the computer by means of the novel technique. The machine comparison with the more established program-synthesis technique of refined A-translation shows a very good performance of Light Dialectica, which is outperformed only in the case of Dickson's Lemma. Also the theory of synthesis of feasible, poly-time computable programs is developed for the new extraction technique. Two pre-existent frameworks due to Cook-Urquhart-Ferreira and respectively Kohlenbach are crossbreeded for this purpose into a "poly-time bounded Analysis". The theoretical result is promising, yet practical examples are to be found for the difference with the pure Kohlenbach's "polynomially bounded Analysis".Cette thèse présente une nouvelle optimisation de l'interprétation fonctionnelle (dite "Dialectica") de Gödel pour l'extraction de programmes plus efficaces à partir de preuves arithmétiques et même analytiques (classiques). La version dite "légère" de Dialectica se combine aussi et encore plus facilement avec l'optimisation dite "monotone" de Kohlenbach sur l'interprétation fonctionnelle de Gödel pour l'extraction de majorants et marges plus efficaces à partir de preuves monotones (classiques). La Dialectica légère est obtenue par l'adaptation des quantificateurs "uniformes" (sans signification computationnelle) de Berger. En plus, sa présentation est faite dans le style de la Déduction Naturelle, comme amélioration de l'adaptation récente de Jørgensen s! ur la Dialectica originelle de Gödel. Un bon nombre d'exemples concrèts sont traités sur l'ordinateur par la nouvelle technique d'extraction de programmes. La comparaison en machine avec la technique de synthèse de programmes appelée "A-traduction raffinée" de Berger, Buchholz et Schwichtenberg montre une très bonne performance de la Dialectica légère. Cette dernière n'est dépassée que dans le cas du Lemme de Dickson. Nous développons aussi la théorie de la synthèse de programmes efficaces, de complexité calculatoire polynômiale en temps, par la nouvelle Dialectica légère (monotone). Dans ce but nous métissons deux structures préexistantes de Cook-Urquhart-Ferreira et respectivement Kohlenbach pour obtenir une "Analyse bornée par des polynômes en temps". Ici, le résultat théorique est prometteur mais des exemple! s pratiques restent encore à trouver pour montrer la diff! ére nce de cette structure par rapport à l'"Analyse bornée par un polynôme" de Kohlenbach