A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

D. Cousineau, A completeness theorem for strong normalization in minimal deduction modulo, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00370379

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

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, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, pp.32-72, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01199506

G. Dowek, T. Hardin, and C. Kirchner, HOL-lambda-sigma: an intentional firstorder 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 and A. Miquel, Cut elimination for Zermelo set theory, manuscript, 2007.

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, Term rewriting and applications, 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

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

J. Girard, Une extension de l'interprétation de Gödeì a l'analyse, et son applicationàplication`plicationà l'´ elimination des coupures dans l'analyse et la théorie des types, nd Scandinavian Logic Symposium, pp.63-92, 1929.

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

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.

P. Amellì-es and B. Werner, A Generic Normalization Proof for Pure Type Systems .Types for proofs and programs. Lecture Notes in Computer Science 1512, 1996.

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, Intentional interpretations of functionals of finite type I. The Journal of Symbolic Logic, pp.198-212, 1967.