This thesis presents a new optimization of Gödel’s Dialectica interpretation for the extraction of more efficient exact realizers from (classical) arithmeti- cal 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 arithmetical and even analytical proofs. “Light Dialec- tica” 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 Dialec- tica. 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 per- formance of Light Dialectica, which is outperformed only in the case of Dick- son’s Lemma. Also the theory of synthesis of feasible, poly-time computable programs is developed for the new “Light Monotone Dialectica” 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”.

This is the unique revision of my PhD thesis, as accepted by the 5-strong Exam committee. Only the French parts were removed. Here is the link to the full thesis https://pastel.archives-ouvertes.fr/pastel-00002286