M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-Calculus Modulo as a Universal Proof Language, 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, International Joint Conference on Automated Reasoning (IJCAR), pp.445-459, 2004.
DOI : 10.1007/978-3-540-25984-8_33

R. Bonichon and O. Hermant, A semantic completeness proof for tableaux modulo, pp.167-181, 2006.

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, Embedding Deduction Modulo into a Prover, Lecture Notes in Computer Science, vol.6247, pp.155-169, 2010.
DOI : 10.1007/978-3-642-15205-4_15

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. Dowek, Truth Values Algebras and Proof Normalization, Lecture Notes in Computer Science, vol.4502, pp.110-124, 2006.
DOI : 10.1007/978-3-540-74464-1_8

G. Dowek, T. Hardin, and C. Kirchner, HOL-????: an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, issue.1, pp.21-45, 2001.
DOI : 10.1017/S0960129500003236
URL : https://hal.archives-ouvertes.fr/hal-01199524

G. Dowek and O. Hermant, A simple proof that super-consistency implies cut elimination, pp.439-456, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00793008

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

H. Friedman, Classically and intuitionistically provably recursive functions
DOI : 10.1007/BFb0103100

G. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol.25, issue.1, p.493565, 1936.
DOI : 10.1007/BF01565428

K. Gödel, Zur intuitionistischen arithmetik und zahlentheorie, Ergebnisse eines mathematischen Kolloquiums, pp.34-38, 1933.

A. Guglielmi, A system of interaction and structure, ACM Transactions on Computational Logic, vol.8, issue.1, pp.1-64, 2007.
DOI : 10.1145/1182613.1182614
URL : https://hal.archives-ouvertes.fr/inria-00441254

O. Hermant, Semantic Cut Elimination in the Intuitionistic Sequent Calculus
DOI : 10.1007/11417170_17

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

M. Jacquel, K. Berkani, D. Delahaye, and C. Dubois, Tableaux Modulo Theories Using Superdeduction, International Joint Conference on Automated Reasoning (IJCAR), pp.332-338, 2012.
DOI : 10.1007/978-3-642-31365-3_26
URL : https://hal.archives-ouvertes.fr/hal-01099338