B. Alarcón, R. Gutiérrez, and S. Lucas, Context-Sensitive Dependency Pairs, LNCS, vol.4337, issue.06, pp.297-308, 2006.

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

T. Arts and J. Giesl, Automatically proving termination where simplification orderings fail, Theory and Practice of Software Development, 1997.
DOI : 10.1007/BFb0030602
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.6946

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

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

F. Blanqui, S. Coupet-grimal, W. Delobel, S. Hinderer, and A. Koprowski, Color, a Coq library on rewriting and termination, Geser and Sondergaard
URL : https://hal.archives-ouvertes.fr/inria-00084835

É. Contejean, The Coccinelle library for rewriting

É. Contejean, A Certified AC Matching Algorithm, LNCS, vol.3091, pp.70-84, 2004.
DOI : 10.1007/978-3-540-25979-4_5

E. Contejean and C. Marché, CiME: Completion modulo E, In Ganzinger [, vol.23, pp.416-419
DOI : 10.1007/3-540-61464-8_70

É. Contejean, C. Marché, B. Monate, and X. Urbain, Proving termination of rewriting with CiME, WST'03, pp.71-73, 2003.

É. Contejean, C. Marché, A. P. Tomás, and X. Urbain, Mechanically Proving Termination Using Polynomial Interpretations, Journal of Automated Reasoning, vol.12, issue.1, pp.325-363, 2005.
DOI : 10.1007/s10817-005-9022-x
URL : https://hal.archives-ouvertes.fr/inria-00001167

É. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain, Certification of Automated Termination Proofs, LNAI, vol.4720, issue.07, pp.148-162, 2007.
DOI : 10.1007/978-3-540-74621-8_10
URL : https://hal.archives-ouvertes.fr/hal-01125312

T. Coquand and C. Paulin-mohring, Inductively defined types, Proceedings of Colog'88, 1988.
DOI : 10.1007/3-540-52335-9_47

P. Courtieu, J. Forest, and X. Urbain, Certifying a Termination Criterion Based on Graphs, without Graphs, LNCS, vol.37, issue.3, pp.183-198, 2008.
DOI : 10.1007/10704567_3
URL : https://hal.archives-ouvertes.fr/hal-01125530

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

N. Dershowitz and J. Jouannaud, Rewrite Systems, pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

J. Endrullis, J. Jambox, J. Endrullis, H. Waldmann, and . Zantema, Matrix Interpretations for Proving Termination of Term Rewriting, Journal of Automated Reasoning, vol.17, issue.4, pp.195-220, 2008.
DOI : 10.1007/s10817-007-9087-9

C. Fuhs, A. Middeldorp, P. Schneider-kamp, and H. Zankl, SAT Solving for Termination Analysis with Polynomial Interpretations, SAT'07, pp.340-354, 2007.
DOI : 10.1007/978-3-540-72788-0_33

J. Giesl, T. Arts, and E. Ohlebusch, Modular Termination Proofs for Rewriting Using Dependency Pairs, Journal of Symbolic Computation, vol.34, issue.1, pp.21-58, 2002.
DOI : 10.1006/jsco.2002.0541
URL : http://doi.org/10.1006/jsco.2002.0541

J. Giesl, R. Thiemann, P. Schneider-kamp, and S. Falke, Improving Dependency Pairs, LPAR'03, volume 2850 of LNAI, pp.165-179, 2003.
DOI : 10.1007/978-3-540-39813-4_11

J. Giesl, P. Schneider-kamp, and R. Thiemann, AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework, LNCS, vol.4130, issue.06, 2006.
DOI : 10.1007/11814771_24

B. Gramlich, On proving termination by innermost termination, Ganzinger [23], pp.93-107
DOI : 10.1007/3-540-61464-8_45

N. Hirokawa and A. Middeldorp, Tyrolean termination tool: Techniques and features, Information and Computation, vol.205, issue.4, pp.474-511, 2007.
DOI : 10.1016/j.ic.2006.08.010

A. Koprowski, TPA: Termination Proved Automatically, LNCS, vol.4098, issue.06, pp.257-266, 2006.
DOI : 10.1007/11805618_19

M. Korp, C. Sternagel, H. Zankl, and A. Middeldorp, Tyrolean Termination Tool 2, RTA'09, pp.295-304, 2009.
DOI : 10.1007/978-3-540-70590-1_23

K. Kusakari, M. Nakamura, and Y. Toyama, Argument Filtering Transformation, PPDP'99, pp.47-61, 1999.
DOI : 10.1007/10704567_3

D. S. Lankford, On proving term rewriting systems are Noetherian, 1979.

C. Marché and H. Zantema, The termination competition 2006, Geser and Sondergaard

Q. H. 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

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

R. Thiemann and C. Sternagel, Certification of Termination Proofs Using CeTA, TPHOLs'09, pp.452-468, 2009.
DOI : 10.1007/978-3-540-25979-4_6

R. Thiemann, J. Giesl, and P. Schneider-kamp, Improved Modular Termination Proofs Using Dependency Pairs, IJCAR'04, pp.75-90, 2004.
DOI : 10.1007/978-3-540-25984-8_4

X. Urbain, Modular and Incremental Automated Termination Proofs, Journal of Automated Reasoning, vol.25, issue.4, pp.315-355, 2004.
DOI : 10.1007/BF03177743