J. Avigad, The computational content of classical arithmetic, Proofs, Categories, and Computations: Essays in Honor of Grigori Mints, pp.15-30, 2010.

M. Baaz and S. Hetzl, Abstract, The Journal of Symbolic Logic, vol.88, issue.01, pp.313-340, 2011.
DOI : 10.1016/B978-044450813-3/50010-2

M. Baaz, S. Hetzl, A. Leitsch, C. Richter, and H. Spohr, Cut-Elimination: Experiments with CERES, Logic for Programming, pp.481-495, 2004.
DOI : 10.1007/978-3-540-32275-7_32

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.93.8096

M. Baaz, S. Hetzl, A. Leitsch, C. Richter, and H. Spohr, CERES: An analysis of F??rstenberg???s proof of the infinity of primes, Theoretical Computer Science, vol.403, issue.2-3, pp.2-3160, 2008.
DOI : 10.1016/j.tcs.2008.02.043

M. Baaz and A. Leitsch, Cut-elimination and Redundancy-elimination by Resolution, Journal of Symbolic Computation, vol.29, issue.2, pp.149-176, 2000.
DOI : 10.1006/jsco.1999.0359

URL : http://doi.org/10.1006/jsco.1999.0359

F. Barbanera and S. Berardi, A Symmetric Lambda Calculus for Classical Program Extraction, Information and Computation, vol.125, issue.2, pp.103-117, 1996.
DOI : 10.1006/inco.1996.0025

H. P. Barendregt, The Lambda Calculus, volume 103 of Studies in Logic and the Foundations of Mathematics, 1984.

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

P. Curien and H. Herbelin, The Duality of Computation, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

V. Danos, J. Joinet, and H. Schellinx, Abstract, The Journal of Symbolic Logic, vol.II, issue.03, pp.755-807, 1997.
DOI : 10.1007/BF00885763

URL : https://hal.archives-ouvertes.fr/inria-00528352

J. Gallier, Constructive logics Part I: A tutorial on proof systems and typed ??-calculi, Theoretical Computer Science, vol.110, issue.2, pp.249-339, 1993.
DOI : 10.1016/0304-3975(93)90011-H

F. Gécseg and M. Steinby, Tree Languages, Handbook of Formal Languages, pp.1-68, 1997.
DOI : 10.1007/978-3-642-59126-6_1

W. Heijltjes, Classical proof forestry Annals of Pure and Applied Logic, pp.1346-1366, 2010.

S. Hetzl, The Computational Content of Arithmetical Proofs, Notre Dame Journal of Formal Logic, vol.53, issue.3
DOI : 10.1215/00294527-1716811

S. Hetzl, On the form of witness terms, Archive for Mathematical Logic, vol.7, issue.4, pp.529-554, 2010.
DOI : 10.1007/s00153-010-0186-7

URL : https://hal.archives-ouvertes.fr/hal-00498696

S. Hetzl, Applying Tree Languages in Proof Theory, Language and Automata Theory and Applications (LATA) 2012, 2012.
DOI : 10.1007/978-3-642-28332-1_26

S. Hetzl, A. Leitsch, and D. Weller, Towards Algorithmic Cut-Introduction, Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), pp.228-242, 2012.
DOI : 10.1007/978-3-642-28717-6_19

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.222.8297

F. Jacquemard, F. Klay, and C. Vacher, Rigid Tree Automata, Third International Conference on Language and Automata Theory and Applications (LATA) 2009, pp.446-457, 2009.
DOI : 10.1007/978-3-540-71389-0_13

URL : https://hal.archives-ouvertes.fr/inria-00579001

F. Jacquemard, F. Klay, and C. Vacher, Rigid tree automata and applications . Information and Computation, pp.486-512, 2011.
DOI : 10.1016/j.ic.2010.11.015

URL : https://hal.archives-ouvertes.fr/inria-00578820

U. Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics, 2008.

R. Mckinley, Herbrand expansion proofs and proof identity In Classical Logic and Computation (CL&C) 2008, participant's proceedings, 2008.

D. Miller, A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-370, 1987.
DOI : 10.1007/BF00370646

M. Parigot, ????-Calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated Reasoning (LPAR) 1992, pp.190-201, 1992.
DOI : 10.1007/BFb0013061

D. Ratiu and T. Trifonov, Exploring the Computational Content of the Infinite Pigeonhole Principle, Journal of Logic and Computation, vol.22, issue.2, pp.329-350, 2012.
DOI : 10.1093/logcom/exq011

C. Urban, Classical Logic and Computation, 2000.

C. Urban and G. Bierman, Strong Normalization of Cut-Elimination in Classical Logic, Fundamenta Informaticae, vol.45, pp.123-155, 2000.

. Zucker, The correspondence between cut-elimination and normalization, Annals of Mathematical Logic, vol.7, issue.1, pp.1-112, 1974.
DOI : 10.1016/0003-4843(74)90010-2