The computational content of classical arithmetic, Proofs, Categories, and Computations: Essays in Honor of Grigori Mints, pp.15-30, 2010. ,
Abstract, The Journal of Symbolic Logic, vol.88, issue.01, pp.313-340, 2011. ,
DOI : 10.1016/B978-044450813-3/50010-2
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
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
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
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
The Lambda Calculus, volume 103 of Studies in Logic and the Foundations of Mathematics, 1984. ,
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
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
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
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
Tree Languages, Handbook of Formal Languages, pp.1-68, 1997. ,
DOI : 10.1007/978-3-642-59126-6_1
Classical proof forestry Annals of Pure and Applied Logic, pp.1346-1366, 2010. ,
The Computational Content of Arithmetical Proofs, Notre Dame Journal of Formal Logic, vol.53, issue.3 ,
DOI : 10.1215/00294527-1716811
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
Applying Tree Languages in Proof Theory, Language and Automata Theory and Applications (LATA) 2012, 2012. ,
DOI : 10.1007/978-3-642-28332-1_26
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
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
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
Applied Proof Theory: Proof Interpretations and their Use in Mathematics, 2008. ,
Herbrand expansion proofs and proof identity In Classical Logic and Computation (CL&C) 2008, participant's proceedings, 2008. ,
A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-370, 1987. ,
DOI : 10.1007/BF00370646
????-Calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated Reasoning (LPAR) 1992, pp.190-201, 1992. ,
DOI : 10.1007/BFb0013061
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
Classical Logic and Computation, 2000. ,
Strong Normalization of Cut-Elimination in Classical Logic, Fundamenta Informaticae, vol.45, pp.123-155, 2000. ,
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