X. Huang, Reconstruction proofs at the assertion level, Proceedings of CADE, pp.738-752, 1994.

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

L. Hallnäs and P. Schroeder-heister, A Proof-Theoretic Approach to Logic Programming, Journal of Logic and Computation, vol.1, issue.5, pp.635-660, 1991.
DOI : 10.1093/logcom/1.5.635

R. Mcdowell and D. Miller, Cut-elimination for a logic with definitions and induction, Theoretical Computer Science, vol.232, issue.1-2, pp.91-119, 2000.
DOI : 10.1016/S0304-3975(99)00171-1

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

J. M. 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

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

H. Cirstea and C. Kirchner, The rewriting calculus - part II, Logic Journal of IGPL, vol.9, issue.3, pp.427-498, 2001.
DOI : 10.1093/jigpal/9.3.377
URL : https://hal.archives-ouvertes.fr/inria-00100532

H. Cirstea, L. Liquori, and B. Wack, Rewriting Calculus with Fixpoints: Untyped and First-Order Systems, In: TYPES, pp.147-161, 2003.
DOI : 10.1007/978-3-540-24849-1_10
URL : https://hal.archives-ouvertes.fr/inria-00100113

C. Urban, Classical Logic and Computation, 2000.

P. Brauner, C. Houtmann, and C. Kirchner, Superdeduction at Work, In: Rewriting, Computation and Proof, pp.132-166, 2007.
DOI : 10.1007/978-3-540-73147-4_7
URL : https://hal.archives-ouvertes.fr/inria-00141672

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/hal-01199506

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

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

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

L. Allali, Algorithmic Equality in Heyting Arithmetic Modulo, In: TYPES, 2007.
DOI : 10.1007/978-3-540-68103-8_1

G. Dowek and A. Miquel, Cut elimination for Zermelo's set theory. Available on author's web page

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/inria-00098847

G. Dowek, Proof normalization for a first-order formulation of higher-order logic, In: TPHOLs, pp.105-119, 1997.
DOI : 10.1007/BFb0028389
URL : https://hal.archives-ouvertes.fr/inria-00073306

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

G. Burel, Unbounded Proof-Length Speed-Up in Deduction Modulo, In: CSL, 2007.
DOI : 10.1007/978-3-540-74915-8_37
URL : https://hal.archives-ouvertes.fr/inria-00138195

G. Burel, Superdeduction as a logical framework, p.8, 2008.

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, Truth Values Algebras and Proof Normalization, In: TYPES, 2006.
DOI : 10.1007/978-3-540-74464-1_8

G. Dowek and O. Hermant, A simple proof that super-consistency implies cut elimination, In: RTA, pp.93-106, 2007.
DOI : 10.1007/978-3-540-73449-9_9
URL : https://hal.archives-ouvertes.fr/hal-00743256

O. Hermant, Méthodes Sémantiques en Déduction Modulo, 2005.

O. Hermant, Semantic Cut Elimination in the Intuitionistic Sequent Calculus, In: TLCA, pp.221-233, 2005.
DOI : 10.1007/11417170_17

G. Burel and C. Kirchner, Cut Elimination in Deduction Modulo by Abstract Completion, In: LFCS, pp.115-131, 2007.
DOI : 10.1007/978-3-540-72734-7_9
URL : https://hal.archives-ouvertes.fr/inria-00115556

G. Dowek, La part du calcul. Mémoire d'habilitation, 1999.

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, p.to TCS, 2008.
DOI : 10.1016/j.tcs.2009.07.041

J. M. Andreoli, Focussing and proof construction, Annals of Pure and Applied Logic, vol.107, issue.1-3, pp.131-163, 2001.
DOI : 10.1016/S0168-0072(00)00032-4
URL : http://doi.org/10.1016/s0168-0072(00)00032-4

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

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

R. Bonichon, TaMeD: A Tableau Method for Deduction Modulo, In: IJCAR, 2004.
DOI : 10.1007/978-3-540-25984-8_33

D. Miller and A. Saurin, From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic, In: CSL, pp.405-419, 2007.
DOI : 10.1007/978-3-540-74915-8_31
URL : https://hal.archives-ouvertes.fr/hal-00527888

P. Brauner, G. Dowek, and B. Wack, Normalization in supernatural deduction and in deduction modulo. Available on the author's webpage, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00141720