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

E. Balland, P. Brauner, R. Kopetz, P. Moreau, and A. Reilles, Tom: Piggybacking Rewriting on Java, Proceedings of RTA, 2007.
DOI : 10.1007/978-3-540-73449-9_5

URL : https://hal.archives-ouvertes.fr/inria-00142045

M. Bezem, D. Hendriks, and H. De-nivelle, Automated Proof Construction in Type Theory Using Resolution, Journal of Automated Reasoning, vol.29, issue.3-4 1, pp.253-275, 2002.
DOI : 10.1007/10721959_10

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

P. Brauner, C. Houtmann, and C. Kirchner, Superdeduction at Work, 2007.
DOI : 10.1007/978-3-540-73147-4_7

URL : https://hal.archives-ouvertes.fr/inria-00141672

G. Burel, Unbounded Proof-Length Speed-Up in Deduction Modulo, 2007.
DOI : 10.1007/978-3-540-74915-8_37

URL : https://hal.archives-ouvertes.fr/inria-00138195

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, Proceedings of TYPES, 2003.
DOI : 10.1007/978-3-540-24849-1_10

URL : https://hal.archives-ouvertes.fr/inria-00100113

D. Cousineau and G. Dowek, Embedding PTS in the ??calculus modulo, Proceedings of TLCA, 2007.

P. Curien and H. Herbelin, The duality of computation, Proceedings of ICFP '00, pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

G. Dowek, Proof normalization for a first-order formulation of higher-order logic, Proceedings of TPHOL, pp.105-119, 1997.
DOI : 10.1007/BFb0028389

URL : https://hal.archives-ouvertes.fr/inria-00073306

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 and A. Miquel, Cut elimination for Zermelo's set theory. Available on author's web page

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
DOI : 10.1007/978-3-540-32033-3_31

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

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

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

Q. Nguyen, C. Kirchner, and H. Kirchner, External rewriting for skeptical proof assistants, Journal of Automated Reasoning, vol.29, issue.3/4, pp.309-336, 2002.
DOI : 10.1023/A:1021975117537

URL : https://hal.archives-ouvertes.fr/inria-00101009

M. Parigot, Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated Reasoning, pp.190-201, 1992.

D. Prawitz, Natural Deduction. A Proof-Theoretical Study, Stockholm Studies in Philosophy. Almqvist & Wiksell, vol.3, issue.2, 1965.

V. Prevosto, Certified mathematical hierarchies: the focal system, Mathematics, Algorithms, Proofs, Dagstuhl Seminar Proceedings, 2005.

C. Urban, Strong normalisation for a Gentzen-like cutelimination procedure, Proceedings of TLCA, pp.415-430, 2001.

C. Urban and G. M. Bierman, Strong Normalisation of Cut-Elimination in Classical Logic, Fundam. Inform, vol.45, issue.4 6, pp.123-155, 2001.
DOI : 10.1007/3-540-48959-2_26

S. Van-bakel, S. Lengrand, and P. Lescanne, The Language ??: Circuits, Computations and Classical Logic, Proceedings of ICTCS'05, pp.81-96, 2005.
DOI : 10.1007/11560586_8

E. Visser and Z. Benaissa, A Core Language for Rewriting, Proceedings of WRLA, 1998.
DOI : 10.1016/S1571-0661(05)80027-1

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