L. Allali and O. Hermant, Semantic A-translations and Super-Consistency Entail Classical Cut Elimination, LNCS ARCoSS, vol.8312, pp.407-422, 2013.
DOI : 10.1007/978-3-642-45221-5_28

T. Altenkirch, M. Hofmann, and T. Streicher, Categorical reconstruction of a reduction free normalization proof, Category Theory and Computer Science, pp.182-199, 1995.
DOI : 10.1007/3-540-60164-3_27

J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

P. B. Andrews, Resolution in type theory, The Journal of Symbolic Logic, vol.34, issue.03, pp.414-432, 1971.
DOI : 10.1073/pnas.49.6.828

Z. M. Ariola, P. Downen, H. Herbelin, K. Nakata, and A. Saurin, Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts, Functional and Logic Programming -11th International Symposium, FLOPS 2012 Proceedings, volume 7294 of Lecture Notes in Computer Science, pp.32-46, 2012.
DOI : 10.1007/978-3-642-29822-6_6
URL : https://hal.archives-ouvertes.fr/hal-00697241

J. Avigad, Algebraic proofs of cut elimination, The Journal of Logic and Algebraic Programming, vol.49, issue.1-2, pp.15-30, 2001.
DOI : 10.1016/S1567-8326(01)00009-1
URL : http://doi.org/10.1016/s1567-8326(01)00009-1

M. Baaz and C. G. Fermüller, Non-elementary speedups between different versions of tableaux, TABLEAUX'95, pp.217-230, 1995.
DOI : 10.1007/3-540-59338-1_38

H. Barendregt, The Lambda Calculus : Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, 1985.

J. Barwise, Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics, 1982.

U. Berger, M. Eberl, and H. Schwichtenberg, Normalisation by evaluation, Prospects for Hardware Foundations, ES- PRIT Working Group, pp.117-137, 1998.

P. W. Bernays12-]-e and . Beth, Reviews. Oiva Ketonen. Untersuchungen zum Pr??dikatenkalkul. Annales Academiae Scientiarum Fennicae, series A, I. Mathematica-physica 23. Helsinki 1944, 71 pp., The Journal of Symbolic Logic, vol.10, issue.04, pp.127-130, 1945.
DOI : 10.2307/2269018

W. Bibel, Automated theorem proving. Artificial intelligence, 1982.

F. Blanqui, J. Jouannaud, and A. Rubio, The Computability Path Ordering: The End of a Quest, Computer Science Logic, 22nd International Workshop 17th Annual Conference of the EACSL Proceedings, volume 5213 of Lecture Notes in Computer Science, pp.1-14, 2008.
DOI : 10.1007/978-3-540-87531-4_1
URL : https://hal.archives-ouvertes.fr/inria-00288209

F. Blanqui, J. Jouannaud, and M. Okada, The Calculus of Algebraic Constructions, Rewriting Techniques and Applications, 1999.
DOI : 10.1007/3-540-48685-2_25
URL : https://hal.archives-ouvertes.fr/inria-00105545

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, Second Workshop on Proof Exchange for Theorem Proving (PxTP), pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

R. Bonichon, TaMeD: A Tableau Method for Deduction Modulo, Automated Reasoning : Second International Joint Conference, 2004.
DOI : 10.1007/978-3-540-25984-8_33
URL : https://hal.archives-ouvertes.fr/hal-01520537

R. Bonichon and O. Hermant, On Constructive Cut Admissibility in Deduction Modulo, TYPES for proofs and programs, pp.33-47, 2006.
DOI : 10.1007/978-3-540-74464-1_3
URL : https://hal.archives-ouvertes.fr/hal-01337639

R. Bonichon and O. Hermant, A Semantic Completeness Proof for TaMeD, Lecture Notes in Computer Science, vol.4246, pp.167-181, 2006.
DOI : 10.1007/11916277_12
URL : https://hal.archives-ouvertes.fr/hal-01337086

R. Bonichon and O. Hermant, Taming tamed. unpublished, 2008.

R. Bonichon and O. Hermant, A syntactic soundness proof for free-variable tableaux with on-the-fly skolemization. unpublished, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01154799

M. Boudard and O. Hermant, Polarizing Double-Negation Translations, LNCS ARCoSS, vol.8312, pp.182-197, 2013.
DOI : 10.1007/978-3-642-45221-5_14
URL : https://hal.archives-ouvertes.fr/hal-00920224

P. Brauner, C. Houtmann, and C. Kirchner, Principles of Superdeduction, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.10-12, 2007.
DOI : 10.1109/LICS.2007.37
URL : https://hal.archives-ouvertes.fr/inria-00133557

A. Brunel, O. Hermant, and C. Houtmann, Orthogonality and Boolean Algebras for Deduction Modulo, Lecture Notes in Computer Science, vol.281, issue.1-2, pp.76-90, 2011.
DOI : 10.1007/BFb0064875
URL : https://hal.archives-ouvertes.fr/inria-00563331

G. Burel, Experimenting with Deduction Modulo, Lecture Notes in Computer Science, vol.43, issue.4, pp.162-176, 2011.
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858

G. Burel and C. Kirchner, Regaining cut admissibility in deduction modulo using abstract completion, Information and Computation, vol.208, issue.2, pp.140-164, 2010.
DOI : 10.1016/j.ic.2009.10.005
URL : https://hal.archives-ouvertes.fr/inria-00132964

G. Bury, D. Delahaye, D. Doligez, P. Halmagrand, and O. Hermant, Automated deduction in the B set theory using typed proof search and deduction modulo, 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning -Short Presentations, LPAR 2015 of EPiC Series in Computing, pp.42-58, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01204701

D. Cantone and M. N. Asmundo, A Further and Effective Liberalization of the delta-Rule in Free Variable Semantic Tableaux, Selected Papers from Automated Deduction in Classical and Non-Classical Logics, pp.109-125, 2000.

Z. Chihani, D. Ilik, and D. Miller, Classical polarizations yield doublenegation translations, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01354298

A. Church, A note on the Entscheidungsproblem, The Journal of Symbolic Logic, vol.166, issue.01, pp.40-41, 1936.
DOI : 10.1007/BF01475439

C. Coquand, From semantics to rules: A machine assisted analysis, CSL, pp.91-105, 1993.
DOI : 10.1007/BFb0049326
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.5491

T. Coquand and J. Gallier, A proof of strong normalization for the theory of constructions using a kripke-like interpretation, Preliminary Proceedings 1st Intl. Workshop on Logical Frameworks, 1990.

R. Cori and D. Lascar, Logique mathématique, 1993.

D. Cousineau, Models and Proof Normalization, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00433165

D. Cousineau, On completeness of reducibility candidates as a semantics of strong normalization, Logical Methods in Computer Science, vol.8, issue.1, p.2012
DOI : 10.2168/LMCS-8(1:3)2012

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, 8th International Conference, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

D. Cousineau and O. Hermant, A semantic proof that reducibility candidates entail cut elimination, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.133-148, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00743284

M. Crabbé, Non-normalisation de ZF. Manuscript, 1974.

D. Cubric, P. Dybjer, and P. J. Scott, Normalization and the Yoneda embedding, Mathematical Structures in Computer Science, vol.8, issue.2, pp.153-192, 1998.
DOI : 10.1017/S0960129597002508

H. B. Curry, The permutability of rules in the classical inferential calculus, The Journal of Symbolic Logic, vol.39, issue.04, pp.245-248, 1952.
DOI : 10.2307/2266612

O. Danvy, Type-Directed Partial Evaluation, Partial Evaluation -Practice and Theory, DIKU 1998 International Summer School, pp.367-411, 1998.
DOI : 10.1007/3-540-47018-2_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.291

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Proof certification in zenon modulo : When achilles uses deduction modulo to outrun the tortoise with shorter steps, IWIL, 10th International Workshop on the Implementation of Logics, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00909688

]. D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Proof compression and certification in zenon modulo, Third Workshop of the Amadeus Project on Proof Compression, 2013.

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, LNCS ARCoSS, vol.8312, pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784

G. Dowek, Truth Values Algebras and Proof Normalization, TYPES for proofs and programs, pp.110-124, 2006.
DOI : 10.1007/978-3-540-74464-1_8

G. Dowek, Polarized deduction modulo, In IFIP Theoretical Computer Science, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.5578

G. Dowek, T. Hardin, and C. Kirchner, Hol-lambda-sigma : an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, pp.1-25, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00098847

G. Dowek, T. Hardin, and C. Kirchner, Binding Logic: Proofs and Models, Lecture Notes in Computer Science, vol.2514, pp.130-144, 2002.
DOI : 10.1007/3-540-36078-6_9
URL : https://hal.archives-ouvertes.fr/inria-00101012

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/inria-00077199

G. Dowek and O. Hermant, A Simple Proof That Super-Consistency Implies Cut Elimination, Lecture Notes in Computer Science, vol.4533, pp.93-106, 2007.
DOI : 10.1007/978-3-540-73449-9_9
URL : https://hal.archives-ouvertes.fr/hal-00150697

G. Dowek and O. Hermant, A Simple Proof that Super-Consistency Implies Cut Elimination, Notre Dame Journal of Formal Logic, vol.53, issue.4, pp.439-456, 2012.
DOI : 10.1215/00294527-1722692
URL : https://hal.archives-ouvertes.fr/hal-00150697

G. Dowek and B. Werner, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116

G. Dowek and B. Werner, Arithmetic as a Theory Modulo, Lecture Notes in Computer Science, vol.3467, pp.423-437, 2005.
DOI : 10.1007/978-3-540-32033-3_31
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.6757

A. G. Dragalin, Mathematical Intuitionism : Introduction to Proof Theory. Translations of mathematical monographs, 1988.

M. A. Dummett, Elements of Intuitionism. Oxford logic guides, 2000.

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, pp.795-807, 1992.
DOI : 10.1007/3-540-54487-9_58

R. Dyckhoff and S. Negri, Abstract, The Journal of Symbolic Logic, vol.94, issue.04, pp.1499-1518, 2000.
DOI : 10.1007/BF01627506

Y. G. Börger and E. Grädel, The Classical Decision Problem, 1997.
DOI : 10.1007/978-3-642-59207-2

M. Fitting, First Order Logic and Automated Theorem Proving, 1996.
DOI : 10.1007/978-1-4612-2360-3

G. Frege, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinenDenkens, p.1879

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

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1934.
DOI : 10.1007/BF01201353

G. Gentzen, Über das Verhaltnis zwischen intuitionistischer une klassischer Logik Archiv für matematische Logik und Grundlagenforschung, pp.119-132, 1974.
DOI : 10.1007/bf02015371

F. Gilbert, A lightweight double-negation translation, 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning -Short Presentations , LPAR 2015, pp.81-93, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01245021

G. Gilbert and O. Hermant, Normalisation by Completeness with Heyting Algebras, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference Proceedings, volume 9450 of Lecture Notes in Computer Science, pp.469-482, 2015.
DOI : 10.1007/978-3-662-48899-7_33

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Girard, P. Taylor, and Y. Lafont, Proofs and Types, 1989.

R. Hähnle and P. Schmitt, The liberalized ?-rule in free variable semantic tableaux, Journal of Automated Reasoning, vol.4, issue.2, pp.211-221, 1994.
DOI : 10.1007/BF00881956

P. Halmagrand, Automated Deduction and Proof Certification for the B Method, Conservatoire National des Arts et Métiers, 1996.
URL : https://hal.archives-ouvertes.fr/tel-01420460

H. Herbelin, Séquents qu'on calcule, 1995.

H. Herbelin and D. Ilik, An analysis of the constructive content of henkin's proof of gödel's completeness theorem, Available on the authors' webpage, 2016.

H. Herbelin, G. Lee, H. Ono, M. Kanazawa, and R. J. De-queiroz, Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus, Logic, Language, Information and Computation Proceedings, volume 5514 of Lecture Notes in Computer Science, pp.209-217, 2009.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/inria-00381554

O. Hermant, A model-based cut elimination proof. 2nd St-Petersburg Days of Logic and Computability, 2003.

O. Hermant, Completeness of cut-free sequent calculus modulo Available on the author's web page, 2004.

O. Hermant, Semantic Cut Elimination in the Intuitionistic Sequent Calculus, Typed Lambda-Calculi and Applications, pp.221-233, 2005.
DOI : 10.1007/11417170_17

O. Hermant, Resolution is Cut-Free, Journal of Automated Reasoning, vol.15, issue.2, pp.245-276, 2010.
DOI : 10.1007/s10817-009-9153-6
URL : https://hal.archives-ouvertes.fr/hal-00743218

O. Hermant and J. Lipton, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, Lecture Notes in Computer Science, vol.5213, pp.169-183, 2008.
DOI : 10.1007/978-3-540-87531-4_14

O. Hermant and J. Lipton, Cut elimination in the Intuitionistic Theory of Types with axioms and rewriting cuts, constructively, Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic and the Foundations of Mathematics, pp.101-134, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00912791

O. Hermant and J. Lipton, Completeness and Cut-elimination in the Intuitionistic Theory of Types--Part 2, Journal of Logic and Computation, vol.20, issue.2, pp.597-602, 2010.
DOI : 10.1093/logcom/exp076
URL : https://hal.archives-ouvertes.fr/hal-00917868

O. Hermant and M. Okada, Cut elimination in higher-order intuitionistic linear logic. unpublished, 2007.

W. Hodges, A Shorter Model Theory, 1997.

C. Houtmann, Representation and interaction of proofs in superdeduction modulo. Theses, 2010.
URL : https://hal.archives-ouvertes.fr/tel-00553219

D. Ilik, Constructive Completeness Proofs and Delimited Control, 2010.
URL : https://hal.archives-ouvertes.fr/tel-00529021

D. Ilik, G. Lee, and H. Herbelin, Kripke models for classical logic, Annals of Pure and Applied Logic, vol.161, issue.11, pp.1367-1378, 2010.
DOI : 10.1016/j.apal.2010.04.007
URL : https://hal.archives-ouvertes.fr/inria-00371959

O. Ketonen, Untersuchungen zum Prädikatenkalkül, 1944.

S. C. Kleene, Introduction to Metamathematics, 1952.

S. C. Kleene, Permutability of inferences in Gentzen's calculi LK and LJ. Memoirs of the, pp.1-26, 1952.

S. C. Kleene, Mathematical logic, 1967.

A. Kolmogorov, On the principle of the excluded middle, Mat. Sb, vol.32, pp.646-667, 1925.

J. Krivine, Une preuve formelle et intuitionniste du théorème de complétude de la logique classique. The Bulletin of Symbolic Logic, pp.405-421, 1996.
DOI : 10.2307/421172

J. Krivine, Realisability in Classical Logic, Course Notes, 2004.

J. Leach and S. Nieva, A Higher-Order Logic Programming Language with Constraints, Lecture Notes in Computer Science, vol.2024, pp.108-122, 2001.
DOI : 10.1007/3-540-44716-4_7

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041
URL : http://doi.org/10.1016/j.tcs.2009.07.041

C. Liang and D. Miller, On subexponentials, synthetic connectives, and multilevel delimited control, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference Proceedings, volume 9450 of Lecture Notes in Computer Science, pp.297-312, 2015.
DOI : 10.1007/978-3-662-48899-7_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.696.2415

J. Lipton and M. Marco, Completeness and cut elimination in Church's intuitionistic theory of types, Journal of Logic and Computation, vol.15, pp.821-854, 2005.

J. Lipton and S. Nieva, Higher-Order Logic Programming Languages with Constraints: A Semantics, Lecture Notes in Computer Science, vol.4583, pp.272-289, 2007.
DOI : 10.1007/978-3-540-73228-0_20

S. Maehara, Eine Darstellung der Intuitionistischen Logik in der Klassischen, Nagoya Mathematical Journal, vol.2, pp.45-64, 1954.
DOI : 10.1007/BF01201353

S. Maehara, Lattice-valued representation of the cut-elimination theorem, Tsukuba Journal of Mathematics, vol.15, issue.2, pp.509-521, 1991.
DOI : 10.21099/tkbjm/1496161672

J. Mitchell, Foundations for Programming Languages, 1996.

J. Mitchell and E. Moggi, Kripke-style models for typed lambda calculus, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.99-124, 1991.
DOI : 10.1016/0168-0072(91)90067-V
URL : http://doi.org/10.1016/0168-0072(91)90067-v

A. Naibo, Le statut dynamique des axiomes. Des preuves aux modèles, 2013.

S. Negri, Sequent calculus proof theory of intuitionistic apartness and order relations, Archive for Mathematical Logic, vol.38, issue.8, pp.521-547, 1999.
DOI : 10.1007/s001530050137

S. Negri and J. Plato, Abstract, Bulletin of Symbolic Logic, vol.4, issue.04, pp.418-435, 1998.
DOI : 10.2307/420956

S. Negri and J. Plato, Proof systems for lattice theory, Mathematical Structures in Computer Science, vol.14, issue.4, pp.507-526, 2004.
DOI : 10.1017/S0960129504004244

A. Nerode and R. A. Shore, Logic for Applications, 1993.

W. Nutt, P. Réty, and G. Smolka, Basic narrowing revisited, Journal of Symbolic Computation, vol.7, issue.3-4, pp.295-317, 1989.
DOI : 10.1016/S0747-7171(89)80014-8
URL : http://doi.org/10.1016/s0747-7171(89)80014-8

M. Okada, Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic, Theoretical Computer Science, vol.227, issue.1-2, pp.333-396, 1999.
DOI : 10.1016/S0304-3975(99)00058-4
URL : http://doi.org/10.1016/s0304-3975(99)00058-4

M. Okada, A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, vol.281, issue.1-2, pp.471-498, 2002.
DOI : 10.1016/S0304-3975(02)00024-5

D. Prawitz, Completeness and Hauptsatz for second order logic1, Theoria, vol.23, issue.3, pp.246-258, 1964.
DOI : 10.1111/j.1755-2567.1967.tb00622.x

D. Prawitz, Hauptsatz for higher order logic, The Journal of Symbolic Logic, vol.25, issue.03, pp.452-457, 1968.
DOI : 10.1090/S0002-9904-1966-11611-7

H. Rasiowa and R. Sikorski, The mathematics of metamathematics. PWN, Polish Scientific Publishers, The Principles of Mathematics, 1903.

R. Saillard, Rewriting Modulo ?? in the ????-Calculus Modulo, Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages : Theory and Practice, LFMTP 2015, pp.87-101, 2015.
DOI : 10.4204/EPTCS.185.6
URL : https://hal.archives-ouvertes.fr/hal-01176715

R. Saillard, Typechecking in the ??-Calculus Modulo : Theory and Practice, Thèse de doctorat, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01299180

J. E. Santo, R. Matthes, and L. Pinto, Continuation-passing style and strong normalisation for intuitionistic sequent calculi, Logical Methods in Computer Science, vol.5, issue.2, 2009.

C. Schürmann and J. Sarnat, Structural Logical Relations, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.24-27, 2008.
DOI : 10.1109/LICS.2008.44

K. Schütte, Schlu???weisen-Kalk???le der Pr???dikatenlogik, Mathematische Annalen, vol.122, issue.1, pp.47-65, 1950.
DOI : 10.1007/BF01342950

K. Schütte, Syntactical and semantical properties of simple type theory, The Journal of Symbolic Logic, vol.15, issue.04, pp.305-326, 1960.
DOI : 10.1007/BF01969991

K. Schütte, Proof Theory. Grundlehren der matematischen Wissenschaften, 1977.

R. M. Smullyan, First-Order Logic, 1968.
DOI : 10.1201/b10689-23

J. Stuber, A Model-Based Completeness Proof of Extended Narrowing and Resolution, First International Joint Conference on Automated Reasoning (IJCAR-2001), pp.195-210, 2001.
DOI : 10.1007/3-540-45744-5_15
URL : https://hal.archives-ouvertes.fr/inria-00100440

M. E. Szabo, Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundation of Mathematics, 1969.

W. W. Tait, A nonconstructive proof of Gentzen's Hauptsatz for second order predicate logic, Bulletin of the American Mathematical Society, vol.72, issue.6, pp.980-983, 1966.
DOI : 10.1090/S0002-9904-1966-11611-7

M. Takahashi, A proof of cut-elimination theorem in simple type-theory, Journal of the Mathematical Society of Japan, vol.19, issue.4, pp.399-410, 1967.
DOI : 10.2969/jmsj/01940399

G. Takeuti, Proof Theory, 1987.

A. S. Troelstra, Lectures on Linear Logic, volume 30 of CSLI Lecture Notes. Center for the Study of Language and Information, 1992.

A. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, vol.42, issue.43, pp.230-265, 1937.

C. Urban, Classical Logic and Computation, 2000.

C. Urban, Strong Normalisation for a Gentzen-like Cut-Elimination Procedure, Proceedings of TLCA, pp.415-430, 2001.
DOI : 10.1007/3-540-45413-6_32
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.134.1306

J. Van-heijenoort, From Frege to Gödel : A Source Book in Mathematical Logic, 1879-1931. Source books in the history of the sciences, 1967.

W. Veldman, An Intuitionistic Completeness Theorem for Intuitionistic Predicate Logic, The Journal of Symbolic Logic, vol.41, issue.1, pp.159-166, 1976.
DOI : 10.2307/2272955

A. Waaler and L. Wallen, Handbook of Tableau Methods, chapter Tableaux for Intutionistic Logics, pp.255-296, 1999.