M. Abadi, L. Cardelli, P. Curien, and J. Lévy, Abstract, Journal of Functional Programming, vol.34, issue.04, pp.375-416, 1991.
DOI : 10.1016/0304-3975(86)90035-6

H. Barendregt, The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics, 1984.

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure patterns type systems, Principles of Programming Languages - POPL2003, 2003.
DOI : 10.1145/640128.604152

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

K. Berkling and E. Fehr, A consistent extension of the lambda-calculus as a base for functional programming languages, Information and Control, vol.55, issue.1-3, pp.89-101, 1982.
DOI : 10.1016/S0019-9958(82)90458-2

R. Bloo and K. Rose, Combinatory reduction systems with explicit substitution that preserve strong nomalisation, Proceedings of the Fifth International Conference on Rewriting Techniques and Application (RTA '96), pp.169-183, 1996.

P. Borovansk´yborovansk´y, Controlling rewriting: study and implementation of a strategy formalism, Electronic Notes in Theoretical Computer Science, vol.15, 1998.

P. Borovansk´yborovansk´y, C. Kirchner, and . Kirchner, A functional view of rewriting and strategies for a semantics of ELAN, The Third Fuji International Symposium on Functional and Logic Programming, pp.143-167, 1998.

P. Borovansk´yborovansk´y, C. Kirchner, P. Héì-ene-kirchner, C. Moreau, and . Ringeissen, An overview of ELAN, Proceedings of Workshop on Rewriting Techniques and Application -WRLA'1998, 1998.

M. Van-den-brand, H. De-jong, P. Klint, and P. Olivier, Efficient annotated terms, Software: Practice and Experience, vol.20, issue.3, pp.259-291, 2000.
DOI : 10.1002/(SICI)1097-024X(200003)30:3<259::AID-SPE298>3.0.CO;2-Y

E. Chailloux, P. Manoury, and B. Pagano, Développement d'applications avec Objective CAML, 2000.

H. Cirstea, Calcul de réécriture : fondements et applications, 2000.

H. Cirstea, G. Faure, and C. Kirchner, A rho-calculus of explicit constraint application, Workshop on Rewriting Logic and Applications, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00095626

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, C. Kirchner, and L. Liquori, Matching Power, Proceedings of Rewriting Techniques and Applications RTA, 2001.
DOI : 10.1007/3-540-45127-7_8

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

H. Cirstea, C. Kirchner, and L. Liquori, Rewriting Calculus with(out) Types, Proceedings of the fourth workshop on rewriting logic and applications, 2002.
DOI : 10.1016/S1571-0661(05)82526-5

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

H. Cirstea, C. Kirchner, L. Liquori, and B. Wack, Rewrite Strategies in the Rewriting Calculus, Proceedings of the Third International Workshop on Reduction Strategies in Rewriting and Programming, 2003.
DOI : 10.1016/S1571-0661(05)82613-1

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

M. Clavel, S. Eker, P. Lincoln, and J. Meseguer, Principles of Maude, Proceedings of the first international workshop on rewriting logic, 1996.
DOI : 10.1016/S1571-0661(04)00034-9

P. Curien, T. Hardin, and J. Lévy, Confluence properties of weak and strong calculi of explicit substitutions, Journal of the ACM, vol.43, issue.2, pp.362-397, 1996.
DOI : 10.1145/226643.226675

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

R. David and B. Guillaume, A ??-calculus with explicit weakening and explicit substitution, Mathematical Structures in Computer Science, vol.11, issue.1, pp.169-206, 2001.
DOI : 10.1017/S0960129500003224

URL : https://hal.archives-ouvertes.fr/hal-00384683

. Nicolas-de-bruijn, Lambda calculus with namefree formulas involving symbols that represent reference transforming mappings, Indagationes Mathematicae, vol.40, pp.348-356, 1978.

G. Nicolas and . De-bruijn, A lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, Indagationes Mathematicae, vol.34, pp.381-392, 1972.

G. Dowek, T. Hardin, and C. Kirchner, Higher Order Unification via Explicit Substitutions, Information and Computation, vol.157, issue.1-2, pp.183-235, 2000.
DOI : 10.1006/inco.1999.2837

URL : https://hal.archives-ouvertes.fr/hal-01199528

S. Eker, Associative-commutative matching via bipartite graph matching, The Computer Journal, vol.38, issue.5, pp.381-399, 1995.
DOI : 10.1093/comjnl/38.5.381

URL : http://comjnl.oxfordjournals.org/cgi/content/short/38/5/381

G. Faure and C. Kirchner, Exceptions in the Rewriting Calculus, Proceedings of Rewriting Techniques and Applications - RTA'2002, pp.66-82, 2002.
DOI : 10.1007/3-540-45610-4_6

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

M. J. Gordon, R. Milner, and C. P. Wadsworth, Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science, vol.78, 1979.
DOI : 10.1007/3-540-09724-4

D. Hendriks and V. Van-oostrom, The ? calculus, Proceedings of Conference on Automated Deduction -CADE'2003, pp.136-150, 2003.

P. Hudak and J. H. Fasel, A gentle introduction to Haskell, ACM SIGPLAN Notices, vol.27, issue.5, pp.1-53, 1992.
DOI : 10.1145/130697.130698

G. Huet, Resolution d'Equations dans les Languages d'Ordre 1, These de Doctorat D'Etat, 1976.

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230

J. Kirchner, Completion of a set of rules modulo a set of equations, SIAM Journal of Computing, vol.15, issue.4, pp.1155-1194, 1986.

D. Kesner and S. Lengrand, Extending the Explicit Substitution Paradigm, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA '05), 2005.
DOI : 10.1007/978-3-540-32033-3_30

URL : https://hal.archives-ouvertes.fr/hal-00148847

C. Kirchner-andhéì-ene and . Kirchner, Rewriting, solving, proving. A preliminary version of a book available at www, 1999.

C. Kirchner-andhéì-ene and . Kirchner, Rule-Based Programming and Proving: The ELAN Experience Outcomes, Ninth Asian Computing Science Conference -ASIAN'04, 2004.
DOI : 10.1007/978-3-540-30502-6_27

C. Kirchner, P. Moreau, and A. Reilles, Formal validation of pattern matching code, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '05, pp.187-197, 2005.
DOI : 10.1145/1069774.1069792

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

J. W. Klop, Combinatory Reduction Systems, Mathematisch Centrum, 1980.

X. Leroy, Compiling functional languages Summer school on Semantics of programming languages, 2002.

P. Lescanne, From ? ? to ? v a journey through calculi of explicit substitutions, Conference Record of POPL '94, pp.60-69, 1994.

C. Liang and G. Nadathur, Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts, Journal of Automated Reasoning, vol.198, issue.1?2, pp.89-132, 2004.
DOI : 10.1007/s10817-004-6885-1

L. Liquori and B. Serpette, iRho, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '04, pp.167-178, 2004.
DOI : 10.1145/1013963.1013983

URL : https://hal.archives-ouvertes.fr/hal-01148883

P. Moreau, C. Ringeissen, and M. Vittek, A Pattern Matching Compiler for Multiple Target Languages, 12th Conference on Compiler Construction, pp.61-76, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099427

C. Muñoz, Un calcul de substitutions pour la représentation de preuves partielles en théorie de types, Thèse de doctorat, 1997.

G. Nadathur, The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations, Ninth Workshop on Logic, Language, Information and Computation Electronic Notes in Theoretical Computer Science, 2002.
DOI : 10.1016/S1571-0661(04)80539-5

Q. Nguyen, C. Kirchner, and . 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

E. Ohlebusch, Church-Rosser theorems for abstract reduction modulo an equivalence relation, Proceedings of Rewriting Techniques and Applications (RTA-98), pp.17-31, 1998.
DOI : 10.1007/BFb0052358

B. Pagano and .. X. , X.R.S: Explicit reduction systems ??? A first-order calculus for higher-order calculi, Proceedings of the International Conference on Automated Deduction (CADE '98), pp.72-87, 1998.
DOI : 10.1007/BFb0054249

URL : https://hal.archives-ouvertes.fr/in2p3-00803707

R. Kristoffer-høgsbro, Operational Reduction Models for Functional Programming Languages, 1996.

F. Sinot, Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting, Journal of Logic and Computation, vol.15, issue.2, pp.201-218, 2005.
DOI : 10.1093/logcom/exi010

M. Stehr, CINNI -A generic calculus of explicit substitutions and its application to lambda-, varsigma-and pi-calculi, Electronic Notes in Theoretical Computer Science, vol.36, 2000.

A. Stump, A. Deivanayagam, S. Kathol, D. Lingelbach, and D. Schobel, Rogue decision procedures, 1st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning -PDPAR 2003, 2003.

B. Wack, Aspects logique du calcul de réécriture, 2005.

H. Yokouchi and T. Hikita, A Rewriting System for Categorical Combinators with Multiple Arguments, SIAM Journal on Computing, vol.19, issue.1, pp.78-97, 1990.
DOI : 10.1137/0219005