R. 1. Allali, Algorithmic equality in Heyting arithmetic modulo. Higher Order Rewriting, 2007.

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

A. Assaf, A Calculus of Constructions with explicit subtyping, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01097401

A. Assaf, Traduction de HOL en Dedukti, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00919871

F. Besson, P. Fontaine, and L. Théry, A Flexible Proof Format for SMT: a Proposal Proof Exchange for Theorem Proving, 2011.

M. Boespflug, Conception d'un noyau de vérification de preuves pour le lambda- Pi-calcul modulo, 2011.

M. Boespflug and G. Burel, CoqInE: translating the calculus of inductive constructions into the lambda-pi-calculus modulo. Proof Exchange for Theorem Proving, pp.44-50, 2012.

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus Modulo as a Universal Proof Language, Proof Exchange for Theorem Proving, CEUR Workshop Proceedings, pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

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

A. Brunel, O. Hermant, and C. Houtmann, Orthogonality and Boolean Algebras for Deduction Modulo. Typed Lambda Calculus and Applications, Lecture Notes in Computer Science, vol.6990, pp.76-90, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00563331

G. Burel, Automating Theories in Intuitionistic Logic, FroCoS, pp.181-197, 2009.
DOI : 10.1016/0168-0072(95)00005-2
URL : https://hal.archives-ouvertes.fr/inria-00395934

G. Burel, Embedding Deduction Modulo into a Prover, CSL, pp.155-169, 2010.
DOI : 10.1007/978-3-642-15205-4_15

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

G. Burel, From Axioms to Rewriting Rules

G. Burel, Cut Admissibility by Saturation. RTA-TLCA, Lecture Notes in Computer Science, vol.8560, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01097428

G. Burel and G. Dowek, How can we prove that a proof search method is not an instance of another? Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, ACM International Conference Proceeding Series, 2009.

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

P. Brauner, C. Houtmann, and C. Kirchner, Superdeduction at Work, Lectures Notes in Computer Science, vol.4600, pp.132-166, 2007.
DOI : 10.1007/978-3-540-73147-4_7
URL : https://hal.archives-ouvertes.fr/inria-00141672

R. Cauderlier, Traits orients objet en ??-calcul modulo : Compilation de FoCaLize vers Dedukti, 2012.

T. Coquand and G. Huet, The calculus of constructions. Information and Computation, pp.95-120, 1988.
URL : https://hal.archives-ouvertes.fr/inria-00076024

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, Lecture Notes in Computer Science, vol.4583, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

M. Crabbé, Non-normalisation de la théorie de Zermelo, 1974.

M. Crabbé, Stratification and cut-elimination. The Journal of Symbolic Logic, pp.213-226, 1991.

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

A. Díaz-caro and G. Dowek, Simply Typed Lambda-Calculus Modulo Type Isomorphism, 2014.

G. Dowek, About Folding-Unfolding Cuts and Cuts Modulo, Journal of Logic and Computation, vol.11, issue.3, pp.419-429, 2001.
DOI : 10.1093/logcom/11.3.419
URL : https://hal.archives-ouvertes.fr/inria-00072640

G. Dowek, What Is a Theory?, Symposium on Theoretical Aspects of Computer Science, pp.50-64, 2002.
DOI : 10.1007/3-540-45841-7_3

G. Dowek, Confluence as a Cut Elimination Property, Rewriting Technique and Applications, pp.2-13, 2003.
DOI : 10.1007/3-540-44881-0_2

G. Dowek, Truth Values Algebras and Proof Normalization, Lectures Notes in Computer Science, vol.4502, 2006.
DOI : 10.1007/978-3-540-74464-1_8

G. Dowek, Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View, Festschrift in Honour of Peter B. Andrews on his 70th Birthday. College Publications, 2008.

G. Dowek, Polarized Resolution Modulo, IFIP Theoretical Computer Science, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : https://hal.archives-ouvertes.fr/hal-01054460

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

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 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-00793008

G. Dowek and A. Miquel, Cut elimination for Zermelo's set theory

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

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

J. Girard, Une extension de l'interprétation de Gödeì a l'analyse et son applicationàtionà l'´ elimination des coupures dans l'analyse et la théorie des types, Second Scandinavian Logic Symposium, 1970.

J. Gao, Clausal Presentation of Theories in Deduction Modulo, Journal of Computer Science and Technology, vol.208, issue.2, pp.1085-1096, 2013.
DOI : 10.1007/s11390-013-1399-0
URL : https://hal.archives-ouvertes.fr/inria-00614251

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

O. Hermant, Semantic Cut Elimination in the Intuitionistic Sequent Calculus, Lecture Notes in Computer Science, vol.3461, 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

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Proceedings of Logic in Computer Science, pp.194-204, 1987.
DOI : 10.1145/138027.138060

G. Huet, A mechanisation of Type Theory, Third International Joint Conference on Artificial Intelligence, pp.139-146, 1973.

G. Huet, A unification algorithm for typed ??-calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-57, 1975.
DOI : 10.1016/0304-3975(75)90011-0

M. Jacquel, K. Berkani, D. Delahaye, and C. Dubois, Tableaux Modulo Theories Using Superdeduction -An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover, IJCAR, pp.332-338, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126134

D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

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

P. Martin-löf, Intuitionistic type theory, Bibliopolis, 1984.

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

M. H. Newman, On Theories with a Combinatorial Definition of "Equivalence", The Annals of Mathematics, vol.43, issue.2, pp.223-243, 1942.
DOI : 10.2307/1968867

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.

G. Plotkin, Building-in equational theories, Machine Intelligence, vol.7, pp.73-90, 1972.

D. Prawitz, Natural Deduction, a Proof-theoretical Study, 1965.

R. Saillard, Towards explicit rewrite rules in the ??-calculus modulo. International Workshop on the Implementation of Logics, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00921340

A. Stump, D. Oe, A. Reynolds, L. Hadarean, and C. Tinelli, SMT proof checking using a logical framework, Formal Methods in System Design, vol.7, issue.1, pp.91-118
DOI : 10.1007/s10703-012-0163-3

J. R. Slagle, Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM, vol.14, issue.4, pp.687-697, 1967.
DOI : 10.1145/321420.321428

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

L. Wos, G. A. Robinson, and D. F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM, vol.12, issue.4, pp.536-541, 1965.
DOI : 10.1145/321296.321302