F. Baader & T. Nipkow (1998):
Term Rewriting and All That.
Cambridge University Press.
J. Giesl & A. Middeldorp (2004):
Transformation Techniques for Context-Sensitive Rewrite Systems.
Journal of Functional Programming 14(4),
pp. 379–427.
J. Giesl, R. Thiemann & P. Schneider-Kamp (2005):
The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs.
In: Proc. LPAR '04,
LNAI 3452,
pp. 301–331.
J. Giesl, R. Thiemann & P. Schneider-Kamp (2005):
Proving and Disproving Termination of Higher-Order Functions.
In: Proc. FroCoS '05,
LNAI 3717,
pp. 216–231.
J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski & R. Thiemann (2010):
Automated Termination Proofs for Haskell by Term Rewriting.
ACM Transactions on Programming Languages and Systems.
To appear. Preliminary version appeared in Proc. RTA '06, LNCS 4098, pp. 297–312, 2006..
B. Gramlich & F. Schernhammer (2010):
Extending Context-Sensitivity in Term Rewriting.
In: Proc. WRS '09,
EPTCS 15,
pp. 56–68.
J. Guttag, D. Kapur & D. Musser (1983):
On Proving Uniform Termination and Restricted Termination of Rewriting Systems.
SIAM Journal of Computation 12,
pp. 189–214.
W. Kurth (1990):
Termination und Konfluenz von Semi-Thue-Systemen mit nur einer Regel.
Ph.D. thesis.
Technische Universität Clausthal, Germany.
D. Lankford & D. Musser (1978):
A Finite Termination Criterion.
Unpublished Draft. USC Information Sciences Institute.
S. Lucas (1998):
Context-Sensitive Computations in Functional and Functional Logic Programs.
Journal of Functional and Logic Programming 1,
pp. 1–61.
S. Lucas (2001):
Termination of On-Demand Rewriting and Termination of OBJ Programs.
In: Proc. PPDP '01,
pp. 82–93.
C. Otto, M. Brockschmidt, C. von Essen & J. Giesl (2010):
Automated Termination Analysis of Java Bytecode by Term Rewriting.
In: Proc. RTA '10,
LIPIcs 6,
pp. 259–276.
É. Payet (2008):
Loop Detection in Term Rewriting Using the Eliminating Unfoldings.
Theoretical Computer Science 403(2-3),
pp. 307–327.
M. Raffelsieper & H. Zantema (2009):
A Transformational Approach to Prove Outermost Termination Automatically.
In: Proc. WRS '08,
ENTCS 237,
pp. 3–21.
M. R. K. Krishna Rao (2000):
Some Characteristics of Strong Innermost Normalization.
Theoretical Computer Science 239,
pp. 141–164.
P. Schneider-Kamp, J. Giesl, A. Serebrenik & R. Thiemann (2009):
Automated Termination Proofs for Logic Programs by Term Rewriting.
ACM Transactions on Computational Logic 11(1).
R. Thiemann, J. Giesl & P. Schneider-Kamp (2008):
Deciding Innermost Loops.
In: Proc. RTA '08,
LNCS 5117,
pp. 366–380.
R. Thiemann (2009):
From Outermost Termination to Innermost Termination.
In: Proc. SOFSEM '09,
LNCS 5404,
pp. 533–545.
R. Thiemann & C. Sternagel (2009):
Loops under Strategies.
In: Proc. RTA '09,
LNCS 5595,
pp. 17–31.
J. Waldmann (2004):
Matchbox: A Tool for Match-Bounded String Rewriting.
In: Proc. RTA '04,
LNCS 3091,
pp. 85–94.
H. Zantema (2005):
Termination of String Rewriting Proved Automatically.
Journal of Automated Reasoning 34,
pp. 105–139.
eptcs@eptcs.org