]. Alv00, R. Andreoli, ]. Maieliand92, and . Andreoli, Reflection for rewriting in the calculus of inductive constructions Focusing and proof-nets in linear and noncommutative logic Logic programming with focusing proofs in linear logic Focussing and proof construction, Proceedings of TYPES 2000 LPAR, volume 1705 of Lecture Notes in Computer ScienceBDW07] P. Brauner, G. Dowek, and B. Wack. Normalization in supernatural deduction and in deduction modulo, pp.321-336297, 1992.

M. Bezem, D. Hendriks, H. De-nivelle-[-bhk07-]-p, C. Brauner, C. Houtmann et al., Automated proof construction in type theory using resolution Principles of superdeduction Inductive Data Type Systems, Proceedings of LICS, pp.3-4253, 2002.

]. G. Bur07 and . Burel, Unbounded proof-length speed-up in deduction modulo, 2007.

G. [. Cousineau, ]. Dowekch00, H. Curien, . Herbelinck01-]-h, C. Cirstea et al., Embedding pure type systems in the lambda-picalculus modulo The duality of computation The rewriting calculus ? Part I and II, TLCA ICFP '00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pp.233-243427, 2000.

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

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo Dowek and A. Miquel. Cut elimination for Zermelo's set theory. Available on author's web page, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519

G. Dowekdw03-]-g, B. Dowek, . [. Werner, B. Dowek, and D. Werner, Proof normalization modulo Arithmetic as a theory modulo, Proceedings of RTA'05 Description of the HOL-SystemJou05] J.-P. Jouannaud. Higher-order rewriting: Framework, confluence and termination. In A. Middeldorp, V. van Oostrom, F. van Raamsdonk, and R. C. de Vrijer Processes, Terms and Cycles, pp.105-1191289, 1993.

H. Kirchner, S. Ranise, C. Ringeissen, and D. Tran, Automatic Combinability of Rewriting-Based Satisfiability Procedures, Lecture Notes in Computer Science Electronic Notes in Theoretical Computer Science, vol.4246, issue.864, pp.542-556, 2003.
DOI : 10.1007/11916277_37
URL : https://hal.archives-ouvertes.fr/inria-00117261

J. Meng, C. Quigley, L. C. Paulson, A. Moreau, and . Reilles, Automation for interactive proof: First prototype. Information and Computation The tom home page, pp.1575-1596, 2006.
DOI : 10.1016/j.ic.2005.05.010
URL : http://doi.org/10.1016/j.ic.2005.05.010

Q. Nguyen, C. Kirchner, H. Kirchner, S. Owre, J. M. Rushby et al., External rewriting for skeptical proof assistants PVS: A prototype verification system, 11th International Conference on Automated Deduction (CADE), pp.3-4309, 1992.

P. Brauner, C. Houtmann, C. Kirchnerpau94, ]. L. Paulson, ]. Isabellepra65 et al., Natural Deduction. A Proof-Theoretical Study, volume 3 of Stockholm Studies in Philosophy Certified mathematical hierarchies: the focal system Schloss Dagstuhl, Germany. [Rud92] P. Rudnicki. An overview of the Mizar project. Notes to a talk at the workshop on Types for Proofs and Programs [The04] The Coq development team. The Coq proof assistant reference manual. LogiCal Project Strong normalisation of cut-elimination in classical logic Strong normalisation for a gentzen-like cut-elimination procedure Visser and Z.-e.-A. Benaissa. A core language for rewriting of Electronic Notes in Theoretical Computer Science, Pont-à-Mousson, France, sep 1998 The language X : circuits, computations and classical logic, of Lecture Notes in Computer Science Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2005. Internationales Begegnungs-und Forschungszentrum (IBFI) TLCA Proceedings of Ninth Italian Conference on Theoretical Computer Science (ICTCS'05). [Wad03] P. Wadler. Call-by-value is dual to call-by-name. In ICFP '03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, pp.123-155, 1965.