B. Alarcón, R. Gutiérrez, and S. Lucas, Context-sensitive dependency pairs, Information and Computation, vol.208, issue.8, pp.922-968, 2010.
DOI : 10.1016/j.ic.2010.03.003

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.
DOI : 10.1016/S0304-3975(99)00207-8

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

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

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

E. Balland, P. Moreau, and A. Reilles, Effective strategic programming for Java developers. Software: Practice and Experience, pp.129-162, 2012.
DOI : 10.1002/spe.2159

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

P. Borovansk´yborovansk´y, C. Kirchner, P. Héì-ene-kirchner, C. Moreau, and . Ringeissen, An overview of ELAN, WRLA '98, 1998.

H. Cirstea, C. Kirchner, R. Kopetz, and P. Moreau, Anti-patterns for rule-based languages, Symbolic Computation in Software Science, pp.523-550, 2010.
DOI : 10.1016/j.jsc.2010.01.007

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

H. Cirstea, S. Lenglet, and P. Moreau, A faithful encoding of programmable strategies into term rewriting systems, RTA '15 Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp.74-88, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01168956

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., The Maude 2.0 System, RTA '03, pp.76-87, 2003.
DOI : 10.1007/3-540-44881-0_7

J. Endrullis and D. Hendriks, From Outermost to Context-Sensitive Rewriting, RTA '09, pp.305-319, 2009.
DOI : 10.1007/978-3-540-95891-8_48

URL : http://dare.ubvu.vu.nl/bitstream/1871/34269/1/243604.pdf

Y. Tomofumi, Alphaz: A system for design space exploration in the polyhedral model, 2012.

F. L. , F. , and L. Maranget, Optimizing pattern matching, ICFP '01, pp.26-37, 2001.

O. Fissore, I. Gnaedig, and . Kirchner, Simplification and termination of strategies in rule-based languages, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming , PPDP '03, pp.124-135, 2003.
DOI : 10.1145/888251.888264

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

C. Fuhs, J. Giesl, M. Parting, P. Schneider-kamp, and S. Swiderski, Proving Termination by Dependency Pairs and Inductive Theorem Proving, Journal of Automated Reasoning, vol.17, issue.1, pp.133-160, 2011.
DOI : 10.1006/jsco.1994.1003

URL : http://www-i2.informatik.rwth-aachen.de/fuhs/papers/JAR11-induction.pdf

J. Giesl and A. Middeldorp, Innermost Termination of Context-Sensitive Rewriting, DLT '02, pp.231-244, 2002.
DOI : 10.1007/3-540-45005-X_20

URL : http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2002/2002-04.ps.gz

J. Giesl and A. Middeldorp, Transformation techniques for context-sensitive rewrite systems, Journal of functional Programming, vol.14, issue.4, pp.379-427, 2004.
DOI : 10.1017/S0956796803004945

URL : http://www.score.is.tsukuba.ac.jp/~ami/research/papers/rta99.ps.gz

J. Giesl, M. Raffelsieper, P. Schneider-kamp, S. Swiderski, and R. Thiemann, Automated termination proofs for haskell by term rewriting, ACM Transactions on Programming Languages and Systems, vol.33, issue.2, p.7, 2011.
DOI : 10.1145/1890028.1890030

J. Giesl, R. Thiemann, and S. Falke, Mechanizing and Improving Dependency Pairs, Journal of Automated Reasoning, vol.34, issue.2, 2006.
DOI : 10.1007/978-1-4757-3661-8

URL : http://www.cs.unm.edu/~spf/papers/JAR06.pdf

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science, 1989.

I. Gnaedig-andhéì-ene and . Kirchner, Termination of rewriting under strategies, ACM Transactions on Computational Logic, vol.10, issue.2, 2009.

A. Gräf, Left-to-right tree pattern matching, RTA '91, pp.323-334, 1991.
DOI : 10.1007/3-540-53904-2_107

N. Hirokawa and A. Middeldorp, Automating the dependency pair method. Information and Computation, pp.172-199, 2005.
DOI : 10.1016/j.ic.2004.10.004

URL : https://doi.org/10.1016/j.ic.2004.10.004

B. Jacobs, Categorical Logic and Type Theory Number 141 in Studies in Logic and the Foundations of Mathematics, 1999.

J. and C. Kirchner, Solving equations in abstract algebras: a rule-based survey of unification, Computational Logic. Essays in honor of Alan Robinson, pp.257-321

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.

M. Kaiser and R. Lämmel, An Isabelle/HOL-based model of stratego-like traversal strategies, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, PPDP '09, pp.93-104, 2009.
DOI : 10.1145/1599410.1599423

M. Korp, C. Sternagel, H. Zankl, and A. Middeldorp, Tyrolean Termination Tool 2, RTA '09, pp.295-304, 2009.
DOI : 10.1007/s10472-009-9144-7

R. Lämmel, S. J. Thompson, and M. Kaiser, Programming errors in traversal programs over structured data, Science of Computer Programming, vol.78, issue.10, pp.1770-1808, 2013.
DOI : 10.1016/j.scico.2011.11.006

M. Manzano, Many-sorted logic and its applications. chapter Introduction to Many-sorted Logic, pp.3-86, 1993.

J. Meseguer and C. Braga, Modular Rewriting Semantics of Programming Languages, Algebraic Methodology and Software Technology, pp.364-378, 2004.
DOI : 10.1007/978-3-540-27815-3_29

P. Moreau, C. Ringeissen, and M. Vittek, A Pattern Matching Compiler for Multiple Target Languages, CC '03, pp.61-76, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099644

E. Ohlebusch, Advanced Topics in Term Rewriting, META-)ENCODINGS OF PROGRAMMABLE STRATEGIES INTO TERM REWRITING SYSTEMS 35, 2002.
DOI : 10.1007/978-1-4757-3661-8

C. Okasaki, Red-black trees in a functional setting, Journal of Functional Programming, vol.9, issue.4, pp.471-477, 1999.
DOI : 10.1017/S0956796899003494

M. Raffelsieper and H. Zantema, A Transformational Approach to Prove Outermost Termination Automatically, Electronic Notes in Theoretical Computer Science, vol.237, pp.3-21, 2009.
DOI : 10.1016/j.entcs.2009.03.032

URL : https://doi.org/10.1016/j.entcs.2009.03.032

G. Rosu and T. Serbanuta, An overview of the K semantic framework, The Journal of Logic and Algebraic Programming, vol.79, issue.6, pp.397-434, 2010.
DOI : 10.1016/j.jlap.2010.03.012

R. Thiemann, From Outermost Termination to Innermost Termination, SOFSEM '09, pp.533-545, 2009.
DOI : 10.1007/978-3-540-70590-1_25

R. Thiemann and A. Middeldorp, Innermost Termination of Rewrite Systems by Labeling, Electronic Notes in Theoretical Computer Science, vol.204, pp.3-19, 2008.
DOI : 10.1016/j.entcs.2008.03.050

E. Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5, RTA '01, pp.357-361, 2001.
DOI : 10.1007/3-540-45127-7_27

E. Visser, A survey of strategies in rule-based program transformation systems, Journal of Symbolic Computation, vol.40, issue.1, pp.831-873, 2005.
DOI : 10.1016/j.jsc.2004.12.011

E. Visser, Z. Benaissa, and A. Tolmach, Building program optimizers with rewriting strategies, ICFP '98, pp.13-26, 1998.
DOI : 10.1145/291251.289425