T. Arts and J. Giesl, Proving innermost normalization automatically, 1996.

T. Arts and J. Giesl, Proving innermost normalisation automatically, Proceedings 8th Conference on Rewriting Techniques and Applications, Sitges (Spain), pp.157-171, 1997.

P. Borovansk´yborovansk´y, C. Kirchner, . Héì, P. Kirchner, C. Moreau et al., Electronic Notes in Theoretical Computer Science, Proceedings of the second International Workshop on Rewriting Logic and Applications, vol.15, pp.98-316, 1998.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., Maude: Specification and programming in rewriting logic, Theoretical Computer Science, vol.285, pp.187-243, 2002.

H. Comon, Disunification: a survey, Computational Logic. Essays in honor of Alan Robinson, pp.322-359, 1991.

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, pp.279-301, 1982.

N. Dershowitz and J. Jouannaud, Handbook of Theoretical Computer Science, Rewrite Systems, vol.B, pp.244-320, 1990.

O. Fissore, I. Gnaedig, and H. Kirchner, Termination of rewriting with local strategies, Selected papers of the 4th International Workshop on Strategies in Automated Deduction, vol.58, 2001.

O. Fissore, I. Gnaedig, and H. Kirchner, CARIBOO : An induction based proof tool for termination with strategies, Proceedings of the Fourth International Conference on Principles and Practice of Declarative Programming, pp.62-73, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00107557

O. Fissore, I. Gnaedig, and H. Kirchner, Outermost ground termination, Proceedings of the Fourth International Workshop on Rewriting Logic and Its Applications, vol.71, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00100755

O. Fissore, I. Gnaedig, and H. Kirchner, Proving weak termination also provides the right way to terminate-Extended version, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00107744

K. Futatsugi and A. Nakagawa, An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks, Proceedings of the 1st IEEE Int, 1997.

I. Gnaedig, H. Kirchner, and O. Fissore, Induction for innermost and outermost ground termination, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00100696

. Goubault-larreck, Well-founded recursive relations, Proc. 15th Int. Workshop Computer Science Logic (CSL'2001), vol.2142, 2001.

J. Goubault-larrecq, A proof of weak termination of typed lambda-sigma-calculi, Proceedings of the TYPES'96 Workshop, vol.1512, 1998.

B. Gramlich, Relating innermost, weak, uniform and modular termination of term rewriting systems, Proceedings of the 3rd International Conference on Logic Programming and Automated Reasoning (LPAR'92), vol.624, pp.285-296, 1992.

B. Gramlich, On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems, Theoretical Computer Science, vol.165, issue.1, pp.97-131, 1996.

G. Huet and J. Lévy, Computations in orthogonal rewriting systems, I, Computational Logic, pp.395-414, 1991.

P. Klint, A meta-environment for generating programming environments, ACM Transactions on Software Engineering and Methodology, vol.2, pp.176-201, 1993.

S. Lucas, Termination of rewriting with strategy annotations, Proc. of 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR'01, vol.2250, pp.669-684, 2001.