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

D. Baelde, On the interaction of minimal generic quantification and fixed points, Logical Frameworks and Meta-languages: Theory and Practice, 2008.

S. C. Bailin, A normalization theorem for set theory, The Journal of Symbolic Logic, pp.673-695, 1988.

H. Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science, pp.117-309, 1992.

S. Berardi, Towards a mathematical analysis of the Coquand-Huet Calculus of Constructions and the other systems in Barendregt's cube, manuscript, 1988.

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, issue.1, pp.37-92, 2005.
DOI : 10.1017/S0960129504004426
URL : https://hal.archives-ouvertes.fr/inria-00105568

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

G. Burel, Bonnes démonstrations en déduction modulo, 2009.

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, pp.56-68, 1940.

M. Crabbé, Non-normalisation de ZF, manuscript, 1974. [11] M. Crabbé, Stratification and cut-elimination, The Journal of Symbolic Logic, pp.213-226, 1991.

T. Coquand and G. Huet, The Calculus of Constructions, Information and Computation, pp.95-120, 1988.

D. Cousineau, Complete reducibility candidates, Proof search in type theory, pp.1-13, 2009.

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Lecture Notes in Computer Science, vol.4583, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

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

G. Dowek, Truth Values Algebras and Proof Normalization, Lecture Notes in Computer Science, vol.4502, pp.110-124, 2007.
DOI : 10.1007/978-3-540-74464-1_8

G. Dowek, . Th, C. Hardin, and . 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/hal-01199506

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

G. Dowek and A. Miquel, Cut elimination for Zermelo set theory, manuscript, 2007.

G. Dowek and B. Werner, Proof normalization modulo, The Journal of Symbolic Logic, pp.1289-1316, 2003.

G. Dowek and B. Werner, Arithmetic as a Theory Modulo, Term rewriting and applications, pp.423-437, 2005.
DOI : 10.1007/978-3-540-32033-3_31

J. Ekman, Normal proofs in set theory, 1994.

M. Fiore, G. Plotkin, and D. Turi, Abstract syntax and variable binding, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.193-202, 1999.
DOI : 10.1109/LICS.1999.782615

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

H. Geuvers and M. J. Nederhof, A modular proof of strong normalization of the calculus of constructions, Journal of Functional Programming, vol.1, issue.2, pp.155-189, 1991.

H. Geuvers, A short and flexible proof of Strong Normalization for the Calculus of Constructions in Types for Proofs and Programs, Int. Workshop TYPES '94, LNCS, vol.996, pp.14-38, 1995.

J. Girard, Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types, 2nd Scandinavian Logic Symposium, pp.63-92, 1971.

L. Hallnäs, On normalization of proofs in set theory, 1983.

M. Hamana, Universal Algebra for Termination of Higher-Order Rewriting, 16th International Conference on Rewriting Techniques and Applications, pp.135-149, 2005.
DOI : 10.1007/978-3-540-32033-3_11

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

L. Henkin, Completeness in the theory of types, The Journal of Symbolic Logic, vol.14, issue.02, pp.81-91, 1950.
DOI : 10.1007/BF01696781

R. , M. Dowell, and D. Miller, Cut-Elimination for a Logic with Definitions and Induction, Theoretical Computer Science, issue.232, pp.91-119, 2000.

O. Hermant, A model based cut elimination proof, nd St-Petersbourg Days in Logic and Computability, 2003.

O. Hermant, Méthodes sémantiques en déduction modulo, 2005.

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

S. Ja?kowski and S. , On the Rules of Supposition in Formal Logic in Studia Logica: Wydawnictwo Po?wi¸econePo?wi¸econe Logice i jej Historii, BIBLIOGRAPHY [38] S. Kripke, A Completeness Theorem in Modal Logic, pp.1-14, 1934.

P. Martin-löf, An intuitionistic type theory of types: predicative part, Logic colloquium, pp.73-118, 1975.

P. A. Melliès and B. Werner, A Generic Normalization Proof for Pure Type Systems, Types for proofs and programs, Lecture Notes in Computer Science, vol.1512, 1996.

B. Nordström, K. Petersson, and J. M. Smith, Martin-Löf's type theory. Handbook of Logic in Computer Science, pp.1-37, 2000.

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

E. Palmgren, On universes in type theory, Twenty five years of constructive type theory, Oxford Logic Guides, pp.191-204, 1998.

D. Prawitz, Hauptsatz for higher order logic. The Journal of Symbolic Logic, pp.452-457, 1968.
DOI : 10.2307/2270331

C. Riba, On the Stability by Union of Reducibility Candidates, 10th International Conference on Foundations of Software Science and Computational Structures, pp.317-331, 2007.
DOI : 10.1007/978-3-540-71389-0_23
URL : https://hal.archives-ouvertes.fr/hal-00123116

W. W. Tait, A non constructive proof of Gentzen's Hauptsatz for second order predicate logic. Bulletin of the, pp.980-983, 1966.

W. W. Tait, Intentional interpretations of functionals of finite type I. The Journal of Symbolic Logic, pp.198-212, 1967.

M. and &. O. 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

J. Terlouw, Een nadere bewijstheoretische analyse van GSTT's, manuscript, 1989.

D. Van-daalen, A description of AUTOMATH and some aspects of its language theory, Synmposium on APL, 1973.

B. Wack, Typage et déduction dans le calcul de réécriture, 2005.