J. Avigad, Formalizing forcing arguments in subsystems of second-order arithmetic, Annals of Pure and Applied Logic, vol.82, issue.2, pp.165-191, 1996.
DOI : 10.1016/0168-0072(96)00003-6

J. Avigad, Interpreting classical theories in constructive ones. The Journal of Symbolic Logic, pp.1785-1812, 2000.

J. Avigad and S. Feferman, G??del???s Functional (???Dialectica???) Interpretation, Handbook of Proof Theory, pp.337-405, 1998.
DOI : 10.1016/S0049-237X(98)80020-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.6017

F. Barbanera and S. Berardi, Extracting constructive content from classical logic via control-like reductions, Typed Lambda Calculi and Applications, pp.45-59, 1993.
DOI : 10.1007/BFb0037097
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.386

J. L. Bates and R. L. Constable, Proofs as programs, ACM Transactions on Programming Languages and Systems, vol.7, issue.1, pp.113-136, 1985.
DOI : 10.1145/2363.2528

A. Beckmann, Abstract, The Journal of Symbolic Logic, vol.103, issue.03, pp.1277-1285, 2001.
DOI : 10.1007/BF01621476

U. Berger, W. Buchholz, and H. Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic, vol.114, issue.1-3, pp.3-25, 2002.
DOI : 10.1016/S0168-0072(01)00073-2
URL : http://doi.org/10.1016/s0168-0072(01)00073-2

U. Berger, M. Eberl, and H. Schwichtenberg, Normalization by Evaluation, Prospects for Hardware Foundations, pp.117-137, 1998.
DOI : 10.1007/3-540-49254-2_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.128.5124

U. Berger, M. Eberl, and H. Schwichtenberg, Term rewriting for normalization by evaluation. Information and Computation, International Workshop on Implicit Computational Complexity (ICC'99). (pp. 135 and 152, pp.19-42, 2003.

U. Berger and H. Schwichtenberg, An inverse of the evaluation functional for typed lambda -calculus, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.203-211, 1991.
DOI : 10.1109/LICS.1991.151645

U. Berger and H. Schwichtenberg, Program extraction from classical proofs, Logic and Computational Complexity, International Workshop LCC '94, pp.77-97, 1994.
DOI : 10.1007/3-540-60178-3_80

U. Berger, H. Schwichtenberg, and M. Seisenberger, The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction, Journal of Automated Reasoning, vol.26, issue.2, pp.205-221, 2001.
DOI : 10.1023/A:1026748613865

M. Bezem, Abstract, The Journal of Symbolic Logic, vol.344, issue.03, pp.652-660, 1985.
DOI : 10.1090/pspum/005/0154801

W. Burr, Functional interpretation of Aczel's constructive set theory, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.31-75, 2000.
DOI : 10.1016/S0168-0072(00)00007-5

R. L. Constable and C. Murthy, Finding computational content in classical proofs, Logical Frameworks, pp.341-362, 1991.
DOI : 10.1017/CBO9780511569807.014

S. Cook, Feasibly constructive proofs and the propositional calculus, Proceedings of the 7th ACM Symposium on the Theory of Computation, pp.83-97, 1975.
DOI : 10.1145/800116.803756

S. Cook and A. Urquhart, Functional interpretations of feasibly constructive arithmetic. Annals of Pure and Applied Logic, pp.103-200, 1993.

T. Coquand and M. Hofmann, A new method for establishing conservativity of classical systems over their intuitionistic version, Mathematical Structures in Computer Science, vol.9, issue.4, pp.323-333, 1999.
DOI : 10.1017/S0960129599002844

J. Diller and W. Nahm, Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen, Archiv f??r Mathematische Logik und Grundlagenforschung, vol.15, issue.1-2, pp.49-66, 1974.
DOI : 10.1007/BF02025118

A. Dragalin, New kinds of realisability and the Markov rule, Russian, the English Translation is, pp.534-537, 1980.

A. Dragalin, New kinds of realisability and the Markov rule, Soviet Math. Dokl, vol.21, pp.461-464, 1980.

S. Feferman, Theories of Finite Type Related to Mathematical Practice, pp.913-972
DOI : 10.1016/S0049-237X(08)71126-1

M. Felleisen, D. P. Friedman, E. Kohlbecker, and B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, vol.52, issue.3, pp.205-237, 1987.
DOI : 10.1016/0304-3975(87)90109-5

M. Felleisen and R. Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, vol.103, issue.2, pp.235-271, 1992.
DOI : 10.1016/0304-3975(92)90014-7

A. Fernandes and F. Ferreira, Abstract, The Journal of Symbolic Logic, vol.two, issue.02, pp.557-578, 2002.
DOI : 10.1016/S0049-237X(98)80054-2

F. Ferreira, A feasible theory for analysis. The Journal of Symbolic Logic, pp.1001-1011, 1994.

F. Ferreira and P. Oliva, Bounded functional interpretation Annals of Pure and Applied Logic, pp.73-112, 2005.

F. Ferreira and P. Oliva, Bounded functional interpretation and feasible analysis, Annals of Pure and Applied Logic, vol.145, issue.2, pp.115-129, 2007.
DOI : 10.1016/j.apal.2006.07.002

H. Friedman, Systems of second order arithmetic with restricted induction, I, II (abstracts) The Journal of Symbolic Logic, pp.557-559, 1976.

H. Friedman, Classically and intuitionistically provably recursive functions, Higher Set Theory, pp.21-27, 1978.
DOI : 10.1007/BFb0103100

P. Gerhardy, Improved Complexity Analysis of Cut Elimination and Herbrand's Theorem. Master's thesis, 2003.

P. Gerhardy, Refined Complexity Analysis of Cut Elimination, Proceedings of the 17th International Workshop CSL 2003, pp.212-225, 2003.
DOI : 10.1007/978-3-540-45220-1_19

P. Gerhardy, The Role of Quantifier Alternations in Cut Elimination, Notre Dame Journal of Formal Logic, vol.46, issue.2, pp.165-171, 2005.
DOI : 10.1305/ndjfl/1117755147

P. Gerhardy and U. Kohlenbach, Extracting Herbrand disjunctions by functional interpretation Archive for Mathematical Logic, pp.633-644, 2005.

P. Gerhardy and U. Kohlenbach, Strongly uniform bounds from semi-constructive proofs, Annals of Pure and Applied Logic, vol.141, issue.1-2, pp.89-107, 2006.
DOI : 10.1016/j.apal.2005.10.003

J. Girard, Interprétation fonctionnelle etéliminationetélimination des coupures dans l'arithmétique d'ordre supérior, p.179, 1972.

J. Girard, P. Taylor, and Y. Lafont, Proofs and Types, pp.25-137, 1989.

T. G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.47-58, 1990.
DOI : 10.1145/96709.96714

P. Hájek, Interpretability and fragments of arithmetic, Arithmetic, proof theory, and computational complexity of Oxford Logic Guides, pp.185-196, 1991.

S. Hayashi and H. Nakano, PX: A Computational Logic, p.180, 1988.

M. Hernest, The MinLog proof-system for Dialectica programextraction . Free software, with full code source and documentation @ http, pp.140-146

M. Hernest, A comparison between two techniques of program extraction from classical proofs Short Contributions and CSL 2003: Extended Posters, volume VIII of Kurt Gödel Society's Collegium Logicum, pp.99-102, 2002.

M. Hernest, Light Functional Interpretation, CSL 2005. (pp. vi, xviii, pp.477-492, 2005.
DOI : 10.1007/11538363_33

M. Hernest, Technical appendix to [51] Available in the author's webpage, p.10, 2005.

M. Hernest, NdE -Normalization during Extraction Computability in Europe Extended Abstract. Full paper in preparation Available in the author's web-page, Local Proceedings of CiE06 (Computability in Europe, pp.79-126, 2006.

M. Hernest, @. Downloadable, and . Http, Light Dialectica Program Extraction from a Classical Fibonacci Proof, Proceedings of DCM'06 at ICALP'06, pp.10-134, 2007.
DOI : 10.1016/j.entcs.2006.10.050

M. Hernest, Synthesis of moduli of uniform continuity by the Monotone Dialectica Interpretation in the proof-system MinLog Accepted for publication, Downloadable @ http, Proceedings of LFMTP'06 at FLoC'06, pp.12-12, 2007.

M. Hernest and U. Kohlenbach, A complexity analysis of functional interpretations Published in a slightly revised form as, pp.129-130, 2003.

M. Hernest and U. Kohlenbach, A complexity analysis of functional interpretations, Theoretical Computer Science, vol.338, issue.1-3, pp.200-246, 2003.
DOI : 10.1016/j.tcs.2004.12.019

W. Howard, Hereditarily majorizable functionals of finite type, [123], pp.454-461

W. Howard, Ordinal analysis of simple cases of bar recursion, The Journal of Symbolic Logic, vol.45, issue.01, pp.17-30, 1981.
DOI : 10.1007/BF02011875

I. Johansson, Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compositio Matematica, vol.4, issue.150, pp.119-136, 1936.

K. Jørgensen, Finite type arithmetic Master's thesis, Departments of Mathematics and Philosophy, vol.13, issue.38, pp.59-76, 2001.

U. Kohlenbach, On the Computational Content of the Krasnoselski and Ishikawa Fixed Point Theorems, pp.119-145
DOI : 10.1007/3-540-45335-0_9

U. Kohlenbach, Proof Interpretations and the Computational Content of Proofs Lecture Course, latest version in the author's web page. (pp. iv, v, vi, vii, x, xi, xvi, xvii, xxi, pp.98-126

U. Kohlenbach, Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. The Journal of Symbolic Logic, pp.1239-1273, 1992.

U. Kohlenbach, Pointwise hereditary majorization and some applications Archive for Mathematical Logic 120 and 151.) [66] U. Kohlenbach. Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, Annals of Pure and Applied Logic, vol.31, issue.64, pp.227-24127, 1992.

U. Kohlenbach, New effective moduli of uniqueness and uniform a?priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numerical Functional Analysis and Optimization, pp.581-606, 1993.

U. Kohlenbach, Analysing proofs in Analysis European Logic Colloquium, Logic: from Foundations to Applications, Keele, pp.225-260, 1993.

U. Kohlenbach, Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals Archive for Mathematical Logic, pp.31-71, 1996.

U. Kohlenbach, Arithmetizing proofs in analysis, Logic Colloquium, pp.115-158, 1996.
DOI : 10.1007/978-3-662-22110-5_5

U. Kohlenbach, Proof interpretations Free downloadble @ http://www.brics.dk/LS/Abs/BRICS- LS-Abs/BRICS-LS-Abs.html. These lecture notes are a polished version of notes from a BRICS PhD course given in the spring term, p.150, 1998.

U. Kohlenbach, Proof theory and computational analysis, Comprox III, Third Workshop on Computation and Approximation Proof theory and computational analysis. (pp. xv, pp.124-157, 1998.
DOI : 10.1016/S1571-0661(05)80219-1

U. Kohlenbach, Abstract, The Journal of Symbolic Logic, vol.36, issue.04, pp.1491-1511, 1999.
DOI : 10.1090/pspum/005/0154801

U. Kohlenbach, A note on Spector's quantifier-free rule of extensionality, Archive for Mathematical Logic, vol.40, issue.2, pp.89-92, 2001.
DOI : 10.1007/s001530000048

U. Kohlenbach, A quantitative version of a theorem due to Borwein-Reich- Shafrir. Numerical Functional Analysis and Optimization, pp.641-656, 2001.

U. Kohlenbach, Uniform asymptotic regularity for Mann iterates, Journal of Mathematical Analysis and Applications, vol.279, issue.2, pp.531-544, 2003.
DOI : 10.1016/S0022-247X(03)00028-3

U. Kohlenbach, Some computational aspects of metric fixed-point theory, Nonlinear Analysis: Theory, Methods & Applications, vol.61, issue.5, pp.823-837, 2005.
DOI : 10.1016/j.na.2005.01.075

U. Kohlenbach, Some Logical Metatheorems with Applications in Functional Analysis, BRICS Report Series, vol.10, issue.21, pp.89-128, 2005.
DOI : 10.7146/brics.v10i21.21791

U. Kohlenbach and B. Lambov, Bounds on Iterations of Asymptotically Quasi-Nonexpansive Mappings, International Conference on Fixed Point Theory and Applications, pp.143-172, 2003.
DOI : 10.7146/brics.v10i51.21823

U. Kohlenbach and L. Leu¸steanleu¸stean, Mann iterates of directionally nonexpansive mappings in hyperbolic spaces, Abstract and Applied Analysis, issue.8, pp.449-477, 2003.

U. Kohlenbach and P. Oliva, Proof Mining: A Systematic Way of Analysing Proofs in Mathematics, Proceedings of the Steklov Institute of Mathematics, pp.136-164, 2003.
DOI : 10.7146/brics.v9i31.21746

U. Kohlenbach and P. Oliva, Proof mining in L1-approximation, Annals of Pure and Applied Logic, vol.121, issue.1, pp.1-38, 2003.
DOI : 10.1016/S0168-0072(02)00081-7

J. Krivine, Classical logic, storage operators and second-order lambda-calculus, Annals of Pure and Applied Logic, vol.68, issue.1, pp.53-78, 1994.
DOI : 10.1016/0168-0072(94)90047-7

D. Leivant, Syntactic translations and provably recursive functions. The Journal of Symbolic Logic, pp.682-688, 1985.

L. Leu¸steanleu¸stean, A quadratic rate of asymptotic regularity for CAT(0)-spaces, Journal of Mathematical Analysis and Applications, vol.325, issue.1, pp.386-399, 2007.
DOI : 10.1016/j.jmaa.2006.01.081

H. Luckhardt, Extensional Gödel Functional Interpretation, Lecture Notes in Mathematics, vol.306, issue.186, pp.224-236, 0197.

H. Luckhardt, Bounds extracted by Kreisel from ineffective proofs, Kreiseliana: About and around Georg Kreisel, pp.289-300, 1996.

C. Murthy, Extracting constructive content from classical proofs, 1990.

C. Murthy, Extracting Constructive Content from Classical Proofs, p.180, 1990.

P. Oliva, Polynomial-time algorithms from ineffective proofs, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.128-137, 2003.
DOI : 10.1109/LICS.2003.1210052

P. Oliva, On Krivine's realizability interpretation of classical second-order arithmetic. To appear in Fundamenta Mathematicae, available in author's home-page, p.147, 2006.

P. Oliva, Understanding and Using Spector???s Bar Recursive Interpretation of Classical Analysis, Proceedings of CiE'2006, pp.423-434, 2006.
DOI : 10.1017/S0027763000010023

P. Oliva, Unifying Functional Interpretations, Notre Dame Journal of Formal Logic, vol.47, issue.2, pp.263-290, 2006.
DOI : 10.1305/ndjfl/1153858651

V. P. Orevkov, Lower bounds on the increase in complexity of deductions after cut elimination, Zap. Nauchn. Sem. Leningrad. Otdel. Mat. Inst. Steklov (LOMI), vol.88, pp.137-162, 1979.

V. P. Orevkov, Complexity of proofs and their transformations in axiomatic theories, Translations of Mathematical Monographs, 1993.

G. Ostrin and S. Wainer, Elementary arithmetic, Annals of Pure and Applied Logic, vol.133, issue.1-3, 2001.
DOI : 10.1016/j.apal.2004.10.012

M. Parigot, ?µ?calculus: an algorithmic interpretation of classical natural deduction, Proc. of Log. Prog. and Automatic Reasoning, pp.190-201, 1992.

C. Parsons, On n-quantifier induction, The Journal of Symbolic Logic, vol.20, issue.03, pp.466-482, 1972.
DOI : 10.1090/pspum/005/0154801

C. Paulin-mohring and B. Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, vol.15, issue.5-6, pp.607-640, 1993.
DOI : 10.1016/S0747-7171(06)80007-6

P. Pudlak, The Lengths of Proofs, pp.547-637
DOI : 10.1016/S0049-237X(98)80023-2

C. Raffalli, Getting results from programs extracted from classical proofs, Theoretical Computer Science, vol.323, issue.1-3, pp.49-70, 2004.
DOI : 10.1016/j.tcs.2004.03.006

P. Rath, Eine verallgemeinerte Funktionalinterpretation der Heyting Arithmetik endlicher Typen, pp.59-187, 1978.

B. Scarpellini, A model for bar recursion of higher types, Compositio Mathematica, vol.23, issue.103, pp.123-153, 1971.

M. Schönfinkel, ???ber die Bausteine der mathematischen Logik, Mathematische Annalen, vol.92, issue.3-4, pp.305-316, 0194.
DOI : 10.1007/BF01448013

H. Schwichtenberg, An arithmetic for polynomial-time computation. To be published by Theoretical Computer Science Available in the author's web page, pp.179-181

H. Schwichtenberg, Minimal logic for computable functions Lecture course on program-extraction from (classical) proofs. Available in the author's web page or in the Minlog distribution, pp.41-44

H. Schwichtenberg, Complexity of normalization in the pure typed lambdacalculus, J. Brouwer, vol.170

H. Schwichtenberg, An upper bound for reduction sequences in the typed ??-calculus, Archive for Mathematical Logic, vol.8, issue.3, pp.405-408, 1991.
DOI : 10.1007/BF01621476

H. Schwichtenberg, Monotone majorizable functionals, Studia Logica, vol.62, issue.2, pp.283-289, 1999.
DOI : 10.1023/A:1026459821186

H. Schwichtenberg and S. Bellantoni, Feasible Computation with Higher Types, Proof and System? Reliability, Proceedings of the NATO Advanced Study Institute, pp.399-415, 2001.
DOI : 10.1007/978-94-010-0413-8_13

H. Schwichtenberg and O. , Proof-and program-extraction system Minlog . Free code and documentation at http://www.minlog-system.de. (pp. xvi, xvii, xviii, pp.140-146

M. Seisenberger, On the Constructive Content of Proofs, p.129, 2003.

S. Simpson, Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic, p.234, 1999.

C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Recursive function theory of Symposia in Pure Mathematics, pp.1-27, 1962.
DOI : 10.1090/pspum/005/0154801

R. Statman, Lower bounds on Herbrand's theorem. Proceedings of the, pp.104-107, 1979.

M. Stein, Interpretation der Heyting-Arithmetik endlicher Typen, pp.59-187, 1976.

A. Troelstra and H. Schwichtenberg, Basic Proof Theory. Number 43 in Cambridge Tracts in Theoretical Computer Science, 2000.