M. Avanzini & G. Moser (2008):
Complexity Analysis by Rewriting.
In: Proc. FLOPS,
pp. 130–146,
doi:10.1007/978-3-540-78969-7_11.
P. Baillot & U. Dal Lago (2016):
Higher-order interpretations and program complexity.
IC,
pp. 56–81,
doi:10.1016/j.ic.2015.12.008.
A. Ben Cherifa & P. Lescanne (1987):
Termination of rewriting systems by polynomial interpretations and its implementation.
Science of Computer Programming 9(2),
pp. 137–159,
doi:10.1016/0167-6423(87)90030-X.
G. Bonfante, A. Cichon, J.-Y. Marion & H. Touzet (2001):
Algorithms with polynomial interpretation termination proof.
Journal of Functional Programming 11(1),
pp. 33–53,
doi:10.1017/S0956796800003877.
G. Bonfante, J. Marion & J. Moyen (2001):
On Lexicographic Termination Ordering with Space Bound Certifications.
In: Proc. PSI,
pp. 482–493,
doi:10.1007/3-540-45575-2_46.
A. Cichon & P. Lescanne (1992):
Polynomial interpretations and the complexity of algorithms.
In: CADE,
pp. 139–147,
doi:10.1007/3-540-55602-8_161.
M. Codish, I. Gonopolskiy, A. M. Ben-Amram, C. Fuhs & J. Giesl (2011):
SAT-based termination analysis using monotonicity constraints over the integers.
Theory and Practice of Logic Programming 11(4-5),
pp. 503–520,
doi:10.1017/S1471068411000147.
E. Contejan, C. Marché, A. P. Tomás & X. Urbain (2005):
Mechanically Proving Termination Using Polynomial Interpretations.
JAR 34(34),
doi:10.1007/s10817-005-9022-x.
Evelyne Contejean, Claude Marché, Ana Paula Tomás & Xavier Urbain (2005):
Mechanically Proving Termination Using Polynomial Interpretations.
JAR 34(4),
pp. 325–363,
doi:10.1007/s10817-005-9022-x.
J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plucker, P. Schneider-Kamp, T. Stroder, S. Swiderski & R. Thiemann (2017):
Analyzing Program Termination and Complexity Automatically with AProVE.
JAR 58,
pp. 3–31,
doi:10.1007/s10817-016-9388-y.
N. Hirokawa & G. Moser (2008):
Automated Complexity Analysis Based on the Dependency Pair Method.
In: Proc. IJCAR,
pp. 364–379,
doi:10.1007/978-3-540-71070-7_32.
D. Hofbauer (1992):
Termination proofs by multiset path orderings imply primitive recursive derivation lengths.
Proc. TCS,
doi:10.1007/3-540-53162-9_50.
D. Hofbauer (2001):
Termination Proofs by Context-Dependent Interpretations.
In: Proc. RTA,
pp. 108–121,
doi:10.1007/3-540-45127-7_10.
D. Hofbauer & C. Lautemann (1989):
Termination proofs and the length of derivations.
In: Proc. RTA,
pp. 167–177,
doi:10.1007/3-540-51081-8_107.
C. Kop & D. Vale (2021):
Tuple Interpretations for Higher-Order Complexity.
In: FSCD,
pp. 31:1–31:22,
doi:10.4230/LIPIcs.FSCD.2021.31.
C. Lautemann (1988):
A note on polynomial interpretation.
Bulletin EATCS volume 36,
pp. 129–131.
F. Mitterwallner & A. Middeldorp (2022):
Polynomial Termination Over N Is Undecidable.
In: Proc. FSCD,
pp. 27:1–27:17,
doi:10.4230/LIPIcs.FSCD.2022.27.
G. Moser (2017):
Uniform Resource Analysis by Rewriting: Strengths and Weaknesses (Invited Talk).
In: Proc. FSCD,
pp. 2:1–2:10,
doi:10.4230/LIPIcs.FSCD.2017.2.
G. Moser, A. Schnabl & J. Waldmann (2008):
Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations.
In: Proc. IARCS,
pp. 304–315,
doi:10.4230/LIPIcs.FSTTCS.2008.1762.
L. Noschinski, F. Emmes & J. Giesl (2011):
A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems.
In: CADE-23,
pp. 422–438,
doi:10.1007/978-3-642-22438-6_32.
J. Steinbach (1992):
Proving polynomials positive.
In: In Proc. FSTTCS 92,
Berlin, Heidelberg,
pp. 191–202,
doi:10.1007/3-540-56287-7_105.
Yoshihito T. (1987):
Counterexamples to termination for the direct sum of term rewriting systems.
Information Processing Letters 25(3),
pp. 141–143,
doi:10.1016/0020-0190(87)90122-0.
A. Weiermann (1995):
Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths.
TCS,
doi:10.1016/0304-3975(94)00135-6.
A. Yamada (2022):
Tuple Interpretations for Termination of Term Rewriting.
J Autom Reasoning,
doi:10.1007s10817-022-09640-4.
eptcs@eptcs.org