@inproceedings(ava:mos:08,
 author       = {M. Avanzini and G. Moser},
 year         = {2008},
 title        = {Complexity Analysis by Rewriting},
 booktitle    = {Proc.\ FLOPS},
 pages        = {130--146},
 doi          = {10.1007/978-3-540-78969-7_11},
)
@article(baillot:lago:16,
 author       = {P. Baillot and Dal Lago, U.},
 year         = {2016},
 title        = {Higher-order interpretations and program complexity},
 journal      = {IC},
 pages        = {56--81},
 doi          = {10.1016/j.ic.2015.12.008},
)
@article(cherifa:lescanne:87,
 author       = {{Ben Cherifa}, A. and P. Lescanne},
 year         = {1987},
 title        = {Termination of rewriting systems by polynomial interpretations and its implementation},
 journal      = {Science of Computer Programming},
 volume       = {9},
 number       = {2},
 pages        = {137--159},
 doi          = {10.1016/0167-6423(87)90030-X},
)
@article(bonfante:cichon:marion:touzet:01,
 author       = {G. Bonfante and A. Cichon and J.-Y. Marion and H. Touzet},
 year         = {2001},
 title        = {Algorithms with polynomial interpretation termination proof},
 journal      = {Journal of Functional Programming},
 volume       = {11},
 number       = {1},
 pages        = {33–53},
 doi          = {10.1017/S0956796800003877},
)
@inproceedings(bonfante:et-al:01,
 author       = {G. Bonfante and J. Marion and J. Moyen},
 year         = {2001},
 title        = {On Lexicographic Termination Ordering with Space Bound Certifications},
 booktitle    = {Proc.\ PSI},
 pages        = {482--493},
 doi          = {10.1007/3-540-45575-2_46},
)
@inproceedings(cichon:lescanne:92,
 author       = {A. Cichon and P. Lescanne},
 year         = {1992},
 title        = {Polynomial interpretations and the complexity of algorithms},
 booktitle    = {CADE},
 pages        = {139--147},
 doi          = {10.1007/3-540-55602-8_161},
)
@article(codish:gonopolskiy:ben-amram:amir:fuhs:giesl:11,
 author       = {M. Codish and I. Gonopolskiy and Ben-Amram, A. M. and C. Fuhs and J. Giesl},
 year         = {2011},
 title        = {SAT-based termination analysis using monotonicity constraints over the integers},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {11},
 number       = {4-5},
 pages        = {503–520},
 doi          = {10.1017/S1471068411000147},
)
@article(contejan:marche:tomas:urbain:05,
 author       = {E. Contejan and C. Marché and A. P. Tomás and X. Urbain},
 year         = {2005},
 title        = {Mechanically Proving Termination Using Polynomial Interpretations},
 journal      = {JAR},
 volume       = {34},
 number       = {34},
 doi          = {10.1007/s10817-005-9022-x},
)
@article(contejan:tomas:urbain:05,
 author       = {Evelyne Contejean and Claude March{\'e} and Ana Paula Tom{\'a}s and Xavier Urbain},
 year         = {2005},
 title        = {Mechanically Proving Termination Using Polynomial Interpretations},
 journal      = {JAR},
 volume       = {34},
 number       = {4},
 pages        = {325--363},
 doi          = {10.1007/s10817-005-9022-x},
)
@article(giesl:et-al:17,
 author       = {J. Giesl and C. Aschermann and M. Brockschmidt and F. Emmes and F. Frohn and C. Fuhs and J. Hensel and C. Otto and M. Plucker and Schneider-Kamp, P. and T. Stroder and S. Swiderski and R. Thiemann},
 year         = {2017},
 title        = {Analyzing Program Termination and Complexity Automatically with \textsf{AProVE}},
 journal      = {JAR},
 volume       = {58},
 pages        = {3--31},
 doi          = {10.1007/s10817-016-9388-y},
)
@inproceedings(nao:moser:08,
 author       = {N. Hirokawa and G. Moser},
 year         = {2008},
 title        = {Automated Complexity Analysis Based on the Dependency Pair Method},
 booktitle    = {Proc.\ IJCAR},
 pages        = {364--379},
 doi          = {10.1007/978-3-540-71070-7_32},
)
@article(hof:92,
 author       = {D. Hofbauer},
 year         = {1992},
 title        = {Termination proofs by multiset path orderings imply primitive recursive derivation lengths},
 journal      = {Proc.\ TCS},
 doi          = {10.1007/3-540-53162-9_50},
)
@inproceedings(hof:01,
 author       = {D. Hofbauer},
 year         = {2001},
 title        = {Termination Proofs by Context-Dependent Interpretations},
 booktitle    = {Proc.\ RTA},
 pages        = {108--121},
 doi          = {10.1007/3-540-45127-7_10},
)
@inproceedings(hof:lau:89,
 author       = {D. Hofbauer and C. Lautemann},
 year         = {1989},
 title        = {Termination proofs and the length of derivations},
 booktitle    = {Proc.\ RTA},
 pages        = {167--177},
 doi          = {10.1007/3-540-51081-8_107},
)
@book(huet:oppen:80,
 author       = {G. Huet and D.C Oppen},
 year         = {1980},
 title        = {Equations and rewrite rules: a survey},
 series       = {Formal Language Theory: Perspectives and Open Problems},
 publisher    = {Loria},
 url          = {http://rewriting.loria.fr/documents/CS-TR-80-785.pdf},
)
@inproceedings(kop:vale:21,
 author       = {C. Kop and D. Vale},
 year         = {2021},
 title        = {{Tuple Interpretations for Higher-Order Complexity}},
 booktitle    = {FSCD},
 pages        = {31:1--31:22},
 doi          = {10.4230/LIPIcs.FSCD.2021.31},
)
@article(lautemann:88,
 author       = {C. Lautemann},
 year         = {1988},
 title        = {A note on polynomial interpretation},
 journal      = {Bulletin EATCS},
 volume       = {volume 36},
 pages        = {129--131},
)
@inproceedings(mitterwallner:aart:22,
 author       = {F. Mitterwallner and A. Middeldorp},
 year         = {2022},
 title        = {{Polynomial Termination Over $\mathbb{N}$ Is Undecidable}},
 booktitle    = {Proc.\ FSCD},
 pages        = {27:1--27:17},
 doi          = {10.4230/LIPIcs.FSCD.2022.27},
)
@inproceedings(moser:17,
 author       = {G. Moser},
 year         = {2017},
 title        = {{Uniform Resource Analysis by Rewriting: Strengths and Weaknesses (Invited Talk)}},
 booktitle    = {Proc.\ FSCD},
 pages        = {2:1--2:10},
 doi          = {10.4230/LIPIcs.FSCD.2017.2},
)
@inproceedings(moser:schnabl:wadmann:08,
 author       = {G. Moser and A. Schnabl and J. Waldmann},
 year         = {2008},
 title        = {{Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations}},
 booktitle    = {Proc.\ IARCS},
 pages        = {304--315},
 doi          = {10.4230/LIPIcs.FSTTCS.2008.1762},
)
@inproceedings(noschinski:emmes:jurgen:11,
 author       = {L. Noschinski and F. Emmes and J. Giesl},
 year         = {2011},
 title        = {A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems},
 booktitle    = {CADE-23},
 pages        = {422--438},
 doi          = {10.1007/978-3-642-22438-6_32},
)
@inproceedings(steinbach:05,
 author       = {J. Steinbach},
 year         = {1992},
 title        = {Proving polynomials positive},
 booktitle    = {In Proc.\ FSTTCS 92},
 address      = {Berlin, Heidelberg},
 pages        = {191--202},
 doi          = {10.1007/3-540-56287-7_105},
)
@article(toyama:87,
 author       = {Yoshihito T.},
 year         = {1987},
 title        = {Counterexamples to termination for the direct sum of term rewriting systems},
 journal      = {Information Processing Letters},
 volume       = {25},
 number       = {3},
 pages        = {141--143},
 doi          = {10.1016/0020-0190(87)90122-0},
)
@article(weiermann:95,
 author       = {A. Weiermann},
 year         = {1995},
 title        = {Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths},
 journal      = {TCS},
 doi          = {10.1016/0304-3975(94)00135-6},
)
@article(yamada:22,
 author       = {A. Yamada},
 year         = {2022},
 title        = {Tuple Interpretations for Termination of Term Rewriting},
 journal      = {J Autom Reasoning},
 doi          = {10.1007s10817-022-09640-4},
)