@inproceedings{abe:06,
  author      = {Abel, A.},
  title       = {Semi-continuous Sized Types and Termination},
  booktitle   = {Proceedings of the 20th International Workshop on Computer Science Logic (CSL '06)},
  year        = {2006},
  editor      = {\'Esik, Z.},
  volume      = {4207},
  series      = {LNCS},
  pages       = {72--88},
  publisher   = {Springer},
}

@unpublished{acz:78,
  author      = {Aczel, P.},
  title       = {A General {C}hurch-{R}osser Theorem},
  year        = {1978},
  note        = {Unpublished Manuscript, University of Manchester.  \url{http://www.ens-lyon.fr/LIP/REWRITING/MISC/AGeneralChurch-RosserTheorem.pdf}}
}

@inproceedings{aba:fou:01,
  author      = {Abadi, M. and Fournet, C.},
  title       = {Mobile values, new names, and secure communication},
  booktitle   = {Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages (POPL '01)},
  year        = {2001},
  editor      = {Hankin, C. and Schmidt, D.},
  pages       = {104--115},
  publisher   = {ACM}
}

@article{abe:04,
  author      = {Abel, A.},
  title       = {Termination checking with types},
  journal     = {Theoretical Informatics and Applications},
  year        = {2004},
  volume      = {38},
  number      = {4},
  pages       = {277--319},
}

@inproceedings{agu:mod:93,
  author      = {Aguzzi, G. and Modigliani, U.},
  title       = {Proving termination of logic programs by transforming them into equivalent term rewriting systems},
  booktitle   = {Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS '93)},
  year        = {1993},
  editor      = {Shyamasundar, R.},
  series      = {LNCS},
  volume      = {761},
  pages       = {114--124},
  publisher   = {Springer},
}

@inproceedings{aka:93,
  author      = {Akama, Y.},
  title       = {On {M}int's reduction for ccc-calculus},
  booktitle   = {Proceedings of the 1st International Conference on Typed Lambda Calculus and Applications ({TLCA} '93)},
  year        = {1993},
  editor      = {Bezem, M. and Groote, J.},
  volume      = {664},
  series      = {LNCS},
  pages       = {1--12},
  publisher   = {Springer},
}

@inproceedings{aot:yam:05,
  author      = {Aoto, T. and Yamada, Y.},
  title       = {Dependency pairs for simply typed term rewriting},
  booktitle   = {Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA '05)},
  year        = {2005},
  editor      = {Giesl, J.},
  volume      = {3467},
  series      = {LNCS},
  pages       = {120--134},
  publisher   = {Springer},
}

@inproceedings{aot:yam:07,
  author      = {Aoto, T. and Yamada, Y.},
  title       = {Argument filterings and usable rules for simply typed dependency pairs (extended abstract)},
  booktitle   = {Proceedings of HOR 2007},
  pages       = {21--27},
  year        = {2007},
  note        = {Workshop proceedings, a preliminary version of \cite{aot:yam:09}}
}

@inproceedings{aot:yam:09,
  author      = {Aoto, T. and Yamada, Y.},
  title       = {Argument filterings and usable rules
               for simply typed dependency pairs},
  booktitle   = {Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS '09)},
  year        = {2009},
  editor      = {Ghilardi, S. and Sebastiani, R.},
  volume      = {5749},
  series      = {LNAI},
  pages       = {117--132},
  publisher   = {Springer},
}

@inproceedings{art:gie:97,
  author      = {Arts, T. and Giesl, J.},
  title       = {Automatically proving termination where simplification orderings fail},
  booktitle   = {Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development (TAPSOFT '97)},
  year        = {1997},
  editor      = {Bidoit, M. and Dauchet, M.},
  volume      = {1214},
  series      = {LNCS},
  pages       = {261--272},
  publisher   = {Springer},
}

@article{art:gie:00,
  author      = {Arts, T. and Giesl, J.},
  title       = {Termination of term rewriting using dependency pairs},
  journal     = {Theoretical Computer Science},
  year        = {2000},
  volume      = {236},
  number      = {1-2},
  pages       = {133--178}
}

@book{baa:nip:98,
  author      = {Baader, F. and Nipkow, F.},
  title       = {Term Rewriting and All That},
  publisher   = {Cambridge University Press},
  year        = {1998},
}

@article{bar:fra:gim:pin:uus:04,
  author      = {Barthe, G. and Frade, M. J. and Gim{\'e}nez, E. and Pinto, L. and Uustalu, T.},
  title       = {Type-based termination of recursive definitions},
  journal     = {Mathematical Structures in Computer Science},
  year        = {2004},
  volume      = {14},
  number      = {1},
  pages       = {97--141},
}

@article{ber:klo:85,
  author      = {Bergstra, J. and Klop, J.W.},
  title       = {Algebra of communicating processes},
  journal     = {Theoretical Computer Science},
  year        = {1985},
  volume      = {37},
  number      = {1},
  pages       = {171--199}
}

@inproceedings{bla:00,
  author      = {Blanqui, F.},
  title       = {Termination and Confluence of Higher-Order Rewrite Systems},
  booktitle   = {Proceedings of the 11th International Conference on Rewriting Techniques and Applications (RTA '00)},
  year        = {2000},
  editor      = {Bachmair, L.},
  volume      = {1833},
  series      = {LNCS},
  pages       = {47-61},
  publisher   = {Springer},
}

@inproceedings{bla:03,
  author      = {Blanqui, F.},
  title       = {Inductive Types in the Calculus of
               Algebraic Constructions},
  booktitle   = {Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications (TLCA '03)},
  year        = {2003},
  editor      = {Hofmann, M.},
  volume      = {2701},
  series      = {LNCS},
  pages       = {46--59},
  publisher   = {Springer},
}

@inproceedings{bla:04,
  author      = {Blanqui, F.},
  title       = {A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems},
  booktitle   = {Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA '04)},
  year        = {2004},
  editor      = {Oostrom, V. van},
  volume      = {3091},
  series      = {LNCS},
  pages       = {24--39},
  publisher   = {Springer},
}

@article{bla:05,
  author      = {Blanqui, F.},
  title       = {Inductive types in the {C}alculus of {A}lgebraic {C}onstructions},
  journal     = {Fundamenta Informaticae},
  year        = {2005},
  volume      = {65},
  number      = {1-2},
  pages       = {61--86},
}

@inproceedings{bla:06,
  author      = {Blanqui, F.},
  title       = {Higher-order dependency pairs},
  booktitle   = {Proceedings of the 8th International Workshop on Termination (WST '06)},
  year        = {2006},
  editor      = {Geser, A. and S/\!\!\!ondergaard, H.},
  pages       = {22--26},
}

@incollection{bla:07,
  author      = {Blanqui, F.},
  title       = {Computability Closure: Ten Years Later},
  booktitle   = {Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of his 60th Birthday},
  year        = {2007},
  editor      = {Comon-Lundh, H. and Kirchner, C. and Kirchner, H.},
  volume      = {4600},
  series      = {LNCS},
  pages       = {68--88},
  publisher   = {Springer},
  note        = {Festschrift}
}

@article{bla:jou:oka:02,
  author      = {Blanqui, F. and Jouannaud, J. and Okada, M.},
  title       = {Inductive-data-type Systems},
  journal     = {Theoretical Computer Science},
  year        = {2002},
  volume      = {272},
  number      = {1-2},
  pages       = {41--68},
}

@inproceedings{bla:jou:rub:08,
  author      = {Blanqui, F. and Jouannaud, J. and Rubio, A.},
  title       = {The Computability Path Ordering: The End of a Quest},
  booktitle   = {Proceedings of the 17th EACSL Annual Conference on Computer Science Logic (CSL '08)},
  year        = {2008},
  editor      = {Kaminski, M. and Martini, S.},
  volume      = {5213},
  series      = {LNCS},
  pages       = {1--14},
  publisher   = {Springer}, 
}

@inproceedings{bla:rib:06,
  author      = {Blanqui, F. and Riba, C.},
  title       = {Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems},
  booktitle   = {Proceedings of the 13th International Conference on Logic for Programming, Artifical Intelligence and Reasoning (LPAR '06)},
  year        = {2006},
  editor      = {Hermann, M. and Voronkov, A.},
  volume      = {4246},
  series      = {LNAI},
  pages       = {105--119},
  publisher   = {Springer},
}

@inproceedings{bla:rou:09,
  author      = {Blanqui, F. and Roux, C.},
  title       = {On the relation between sized-types based termination and semantic labelling},
  booktitle   = {Proceedings of the 23rd International Workshop on Computer Science Logic and the 18th Annual Conference of the EACSL (CSL/EACSL '09)},
  year        = {2009},
  editor      = {Gr\"adel, E. and Kahle, R.},
  volume      = {5771},
  series      = {LNCS},
  pages       = {147--162},
  publisher   = {Springer},
}

@article{bof:bor:rod:rub:12,
  author      = {Bofill, M. and Borralleras, C. and Rodr\'iguez-Carbonell, E. and Rubio, A.},
  title       = {The recursive path and polynomial ordering for first-order and higher-order terms},
  journal     = {Journal of Logic and Computation},
  year        = {2012},
  volume      = {23},
  number      = {1},
  pages       = {263--305},
}

@article{bor:luc:oli:rod:rub:12,
  author      = {Borralleras, C. and Lucas, S. and Oliveras, A. and {Rodr\'{\i}guez-Carbonell}, E. and Rubio, A.}, 
  title       = {{SAT} Modulo Linear Arithmetic for Solving Polynomial Constraints},
  journal     = {Journal of Automated Reasoning},
  year        = {2012},
  volume      = {48},
  number      = {1}, 
  pages       = {107--131},
}

@inproceedings{bor:rub:01,
  author      = {Borralleras, C. and Rubio, A.},
  title       = {A Monotonic Higher-Order Semantic Path Ordering},
  booktitle   = {Proceedings of the 8th International Conference on Logic for Programming, Artifical Intelligence and Reasoning (LPAR '01)},
  year        = {2001},
  editor      = {Nieuwenhuis, R. and Voronkov, A.},
  volume      = {2250},
  series      = {LNAI},
  pages       = {531--547},
  publisher   = {Springer},
}

@incollection{bor:rub:07,
  author      = {Borralleras, C. and Rubio, A.},
  title       = {Orderings and Constraints: Theory and Practice of Proving Termination},
  booktitle   = {Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of his 60th Birthday},
  year        = {2007},
  editor      = {Comon-Lundh, H. and Kirchner, C. and Kirchner, H.},
  volume      = {4600},
  series      = {LNCS},
  pages       = {28--43},
  publisher   = {Springer},
  note        = {Festschrift}
}

@inproceedings{bou:jac:08,
  author    = {Bouhoula, A. and Jacquemard, F.},
  title     = {Automated Induction with Constrained Tree Automata},
  booktitle = {Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR '08)},
  year      = {2008},
  series    = {LNCS},
  volume    = {5195},
  pages     = {539--554},
  publisher = {Springer},
}

@incollection{bro:ott:ess:gie:10,
  author      = {Brockschmidt, M. and Otto, C. and Essen, C. von and Giesl, J\"uergen},
  title       = {Termination Graphs for Java Bytecode},
  booktitle   = {Verification, Induction, Termination Analysis},
  series      = {LNCS},
  editor      = {Siegler, S. and Wasser, N.},
  publisher   = {Springer},
  pages       = {17--37},
  volume      = {6463},
  year        = {2010}
}

@inproceedings{bro:ott:gie:11,
  author      = {Brockschmidth, M. and Otto, C. and Giesl, J},
  title       = {Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting},
  booktitle   = {Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11)},
  year        = {2011},
  editor      = {Schmidt-Schau\ss},
  series      = {LIPIcs},
  volume      = {10},
  pages       = {155--170},
  publisher   = {Dagstuhl},
}

@phdthesis{bru:08,
  author      = {Bruggink, H.J.S.}, 
  title       = {Equivalence of Reductions in Higher-Order Rewriting},
  school      = {Utrecht University},
  year        = {2008}
}

@article{cag:hin:98,
  author      = {\c{C}\!a\u{g}man, N. and Hindley, J.R.},
  title       = {Combinatory weak reduction in lambda-calculus},
  journal     = {Theoretical Computer Science},
  year        = {1998},
  volume      = {198},
  number      = {1-2},
  pages       = {239--247}
}

@article{cod:gie:sch:thi:11,
  author      = {Codish, M. and Giesl, J. and Schneider-Kamp, P. and Thiemann, R.},
  title       = {{SAT} Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs},
  journal     = {Journal of Automated Reasoning},
  year        = {2012},
  volume      = {49},
  number      = {1},
  pages       = {53--93},
}

@article{con:mar:tom:urb:05,
  author      = {Contejean, E. and March{\'e}, C. and Tom{\'a}s, A. and Urbain, X.},
  title       = {Mechanically proving termination using polynomial interpretations},
  journal     = {Journal of Automated Reasoning},
  year        = {2005},
  volume      = {34}, 
  number      = {4},
  pages       = {325--363},
}

@inproceedings{coq:pau:88,
  author      = {Coquand, T. and Paulin-Mohring, C.},
  title       = {Inductively defined types},
  booktitle   = {Proceedings of the International Conference on Computer Logic ({COLOG} '88)},
  year        = {1990},
  editor      = {Martin-L\"of, P. and Mints, G.},
  volume      = {417},
  series      = {LNCS},
  pages       = {50--66},
  publisher   = {Springer},
}

@inproceedings{cos:kes:93,
  author      = {Cosmo, R. and Kesner, D.},
  title       = {A confluent reduction for the extensional typed $\lambda$-calculus with pairs, sums, recursion and terminal object},
  booktitle   = {Proceedings of the 20th International Colloquium on Automata, Languages and Programming (ICALP '93)},
  year        = {1993},
  editor      = {Lingas, A. and Karlsson, R. and Carlsson, S.},
  volume      = {700},
  series      = {LNCS},
  pages       = {645--656},
  publisher   = {Springer},
}

@article{der:82,
  author      = {Dershowitz, N.},
  title       = {Orderings for term rewriting systems},
  journal     = {Theoretical Computer Science},
  year        = {1982},
  volume      = {17},
  number      = {3},
  pages       = {279--301}
}

@inproceedings{der:04,
  author      = {Dershowitz, N.},
  title       = {Termination by abstraction},
  booktitle   = {Proceedings of the 20th International Conference on Logic Programming (ICLP '04)},
  year        = {2004},
  editor      = {Dernoen, B. and Lifschitz, V.},
  volume      = {3132},
  series      = {LNCS},
  pages       = {1--18},
  publisher   = {Springer},
}

@inproceedings{emm:eng:gie:12,
  author      = {Emmes, F. and Enger, T. and Giesl, J.},
  title       = {Proving Non-Looping Non-Termination Automatically},
  booktitle   = {Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR '12)},
  year        = {2012},
  editor      = {Gramlich, B. and Miller, D. and Sattler, U.},
  volume      = {7364},
  series      = {LNAI},
  pages       = {225--240},
  publisher   = {Springer},
}

@article{end:wal:zan:08,
  author      = {Endrullis, J. and Waldmann, J. and Zantema, H.},
  title       = {Matrix Interpretations for Proving Termination of Term Rewriting},
  journal     = {Journal of Automated Reasoning},
  year        = {2008},
  volume      = {40},
  number      = {2-3},
  pages       = {195--220},
}

@inproceedings{een:sor:04,
  author      = {E{\'en}, N. and S{\"o}rensson, N.},
  title       = {An Extensible {SAT}-solver},
  booktitle   = {Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT '03)},
  year        = {2004},
  editor      = {Giunchiglia, E. and Tacchella, A.},
  volume      = {2919},
  series      = {LNCS},
  pages       = {502--518},
  publisher   = {Springer},
  note        = {See also \url{http://minisat.se/}.},
}
@inproceedings{fal:kap:09,
  author      = {Falke, S. and Kapur, D.},
  title       = {A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs},
  booktitle   = {Proceedings of the 22nd International Conference on Automated Deduction (CADE '09)},
  year        = {2009},
  editor      = {Schmidt, R.},
  series      = {LNCS},
  volume      = {5663},
  pages       = {277-293},
  publisher   = {Springer},
}

@inproceedings{fal:kap:12,
  author      = {Falke, S. and Kapur, D.},
  title       = {Rewriting Induction + Linear Arithmetic = Decision Procedure},
  booktitle   = {Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR '12)},
  year        = {2012},
  editor      = {Gramlich, B. and Miller, D. and Sattler, U.},
  series      = {LNAI},
  volume      = {7364},
  pages       = {241--255},
  publisher   = {Springer},
}

@inproceedings{fal:kap:sin:11,
  author      = {Falke, S. and Kapur, D. and Sinz, C.},
  title       = {Termination Analysis of C Programs Using Compiler Intermediate Languages},
  booktitle   = {Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11)},
  year        = {2011},
  editor      = {Schmidt-Schau{\ss}, M.},
  series      = {LIPIcs},
  volume      = {10},
  pages       = {41--50},
  publisher   = {Dagstuhl},
}

@inproceedings{fal:kap:sin:12,
  author      = {Falke, S. and Kapur, D. and Sinz, C.},
  title       = {Termination Analysis of Imperative Programs Using Bitvector Arithmetic},
  booktitle   = {Proceedings of the 4th International Conference on Verified Software: Theories, Tools and Experiments (VSTTE '12)},
  year        = {2012},
  editor      = {Joshi, R.\ and M\"uller, P. and Podelski, A.},
  series      = {LNCS},
  volume      = {7152},
  pages       = {261--277},
  publisher   = {Springer},
}

@inproceedings{fer:zan:94,
  author      = {Ferreira, M. and Zantema, H.},
  title       = {Syntactical analysis of total termination},
  booktitle   = {Proceedings of the 4th International Conference on Algebraic and Logic Programming (ALP '94)},
  year        = {1994},
  editor      = {Levi, G. and Rodr\'iguez-Artalejo, M.},
  volume      = {850},
  series      = {LNCS},
  pages       = {204--222},
  publisher   = {Springer},
}

@inproceedings{fuh:gie:mid:sch:thi:zan:07,
  author      = {Fuhs, C. and Giesl, J. and Middeldorp, A. and Schneider-Kamp, P. and Thiemann, R. and Zankl, H.},
  title       = {{SAT} Solving for Termination Analysis with Polynomial Interpretations},
  booktitle   = {Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT '07)},
  year        = {2007},
  editor      = {Marques-Silva, J. and Sakallah, K.},
  volume      = {4501},
  series      = {LNCS},
  pages       = {340--354},
  publisher   = {Springer},
}

@inproceedings{fuh:gie:mid:sch:thi:zan:08,
  author      = {Fuhs, C. and Giesl, J. and Middeldorp, A. and {Schneider-Kamp}, P. and Thiemann, R. and Zankl, H.}, 
  title       = {Maximal Termination},
  booktitle   = {Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA '08)},
  year        = {2008},
  editor      = {Voronkov, A.},
  volume      = {5117},
  series      = {LNCS},
  pages       = {110--125},
  publisher   = {Springer},
}

@article{fuh:gie:par:sch:swi:11,
  author      = {Fuhs, C. and Giesl, J. and Parting, M. and Schneider-Kamp, P. and Swiderski, S.},
  title       = {Proving Termination by Dependency Pairs and Inductive Theorem Proving},
  journal     = {Journal of Automated Reasoning},
  year        = {2011},
  volume      = {47},
  number      = {2},
  pages       = {133--160},
}

@inproceedings{fuh:gie:plu:sch:fal:09,
  author      = {Fuhs, C. and Giesl, J. and Pl{\"u}cker, M. and {Schneider-Kamp}, P. and Falke, S.},
  title       = {Proving Termination of Integer Term Rewriting},
  booktitle   = {Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09)},
  year        = {2009},
  editor      = {Treinen, R.},
  volume      = {5595},
  series      = {LNCS},
  pages       = {32--47},
  publisher   = {Springer},
}

@inproceedings{fuh:kop:11,
  author      = {Fuhs, C. and Kop, C.},
  title       = {Harnessing First Order Termination Provers Using Higher Order Dependency Pairs},
  booktitle   = {Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS '11)},
  year        = {2011},
  editor      = {Tinelli, C. and Sofronie-Stokkermans, V.},
  volume      = {6989},
  series      = {LNAI},
  pages       = {147--162},
  publisher   = {Springer},
}

@inproceedings{fuh:kop:12,
  author      = {Fuhs, C. and Kop, C.},
  title       = {Polynomial Interpretations for Higher-order Rewriting},
  booktitle   = {Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA '12)},
  year        = {2012},
  editor      = {Tiwari, A.},
  volume      = {15},
  series      = {LIPIcs},
  pages       = {176--192},
  publisher   = {Dagstuhl},
}

@article{fur:nis:sak:kus:sak:08,
  author      = {Furuichi, Y. and Nishida, N. and Sakai, M. and Kusakari, K. and Sakabe, T.},
  title       = {Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems},
  journal     = {IPSJ Transactions on Programming},
  volume      = {1},
  number      = {2},
  pages       = {100--121},
  year        = {2008},
  note        = {In Japanese},
}

@article{ges:hof:wal:04,
  author      = {Geser, A. and Hofbauer, D. and Waldmann, J.},
  title       = {Match-Bounded String Rewriting Systems},
  journal     = {Applicable Algebra in Engineering, Communication and Computing},
  year        = {2004},
  volume      = {15},
  number      = {3},
  pages       = {149--171},
}

@article{gie:art:ohl:02,
  author      = {Giesl, J. and Arts, T. and Ohlebusch, E.},
  title       = {Modular Termination Proofs for Rewriting Using Dependency Pairs},
  journal     = {Journal of Symbolic Computation},
  year        = {2002},
  volume      = {34},
  number      = {1},
  pages       = {21--58}
}

@article{gie:raf:sch:swi:thi:11,
  author      = {Giesl, J. and Raffelsieper, M. and Schneider-Kamp, P. and Swiderski, S. and Thiemann, R.},
  title       = {Automated Termination Proofs for {H}askell by Term Rewriting},
  journal     = {ACM Transactions on Programming Languages and Systems},
  year        = {2011},
  volume      = {33},
  number      = {2},
  pages       = {7:1--7:39},
}

@inproceedings{gie:sch:thi:06,
  author      = {Giesl, J. and Schneider-Kamp, P. and Thiemann, R.},
  title       = {{AProVE 1.2}: Automatic termination proofs in the dependency pair framework},
  booktitle   = {Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR '06)},
  year        = {2006},
  editor      = {Furbach, U. and Shankar, N.},
  volume      = {4130},
  series      = {LNAI},
  pages       = {281--286},
  publisher   = {Springer},
}

@inproceedings{gie:thi:sch:05:1,
  author      = {Giesl, J. and Thiemann, R. and Schneider-Kamp, P.},
  title       = {Proving and disproving termination of higher-order functions},
  booktitle   = {Proceedings of the 5th International Symposium on Frontiers of Combining Systems (FroCoS '05)},
  year        = {2005},
  editor      = {Gramlich, B.},
  volume      = {3717},
  series      = {LNAI},
  pages       = {216--231},
  publisher   = {Springer},
}

@incollection{gie:thi:sch:05:2,
  author      = {Giesl, J. and Thiemann, R. and Schneider-Kamp, P.},
  title       = {The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs},
  booktitle   = {Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '04)},
  year        = {2005},
  editor      = {Baader, F. and Voronkov, A.},
  volume      = {3452},
  series      = {LNAI},
  pages       = {301--331},
  publisher   = {Springer}
}

@article{gie:thi:sch:fal:06,
  author      = {Giesl, J. and Thiemann, R. and Schneider-Kamp, P. and Falke, S.},
  title       = {Mechanizing and Improving Dependency Pairs},
  journal     = {Journal of Automated Reasoning},
  year        = {2006},
  volume      = {37},
  number      = {3},
  pages       = {155--203},
}

@inproceedings{gie:thi:swi:sch:07,
  author      = {Giesl, J. and Thiemann, R. and Swiderski, S. and {Schneider-Kamp}, P.},
  title       = {Proving Termination by Bounded Increase},
  booktitle   = {Proceedings of the 21st International Conference on Automated Deduction (CADE '07)},
  year        = {2007},
  editor      = {Pfenning, F.},
  volume      = {4603},
  series      = {LNAI},
  pages       = {443--459},
  publisher   = {Springer},
}

@inproceedings{gim:98,
  author      = {Gim\'enez, E.},
  title       = {Structural recursive definitions in type theory},
  booktitle   = {Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP '98)},
  year        = {1998},
  editor      = {Larsen, K. and Skyum, S. and Winskel, G.},
  series      = {LNCS},
  volume      = {1443},
  pages       = {397--408},
  publisher   = {Springer},
}

@article{gra:95,
  author      = {Gramlich, B.},
  title       = {Abstract Relations between Restricted Termination and Confluence Properties of Rewrite Systems},
  journal     = {Fundamenta Informaticae},
  year        = {1995},
  volume      = {24},
  number      = {1-2},
  pages       = {3--23}
}

@inproceedings{ham:07,
  author      = {Hamana, M.},
  title       = {Higher-order semantic labelling for inductive datatype systems},
  booktitle   = {Proceedings of the 9th ACM SIGPLAN International Conference on Principles and practice of declarative programming (PPDP '07)},
  year        = {2007},
  editor      = {Leuschel, M. and Podelski, A.},
  pages       = {97--108},
  publisher   = {ACM},
}

@inproceedings{hir:mid:04,
  author      = {Hirokawa, N. and Middeldorp, A.},
  title       = {Dependency Pairs Revisited},
  booktitle   = {Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA '04)},
  year        = {2004},
  editor      = {Oostrom, V. van},
  volume      = {3091},
  series      = {LNCS},
  pages       = {249--268},
  publisher   = {Springer},
}

@article{hir:mid:05,
  author      = {Hirokawa, N. and Middeldorp, A.},
  title       = {Automating the dependency pair method},
  journal     = {Information and Computation},
  year        = {2005},
  volume      = {199},
  number      = {1-2},
  pages       = {172--199},
}

@article{hir:mid:07,
  author      = {Hirokawa, N. and Middeldorp, A.},
  title       = {Tyrolean termination tool: Techniques and features},
  journal     = {Information and Computation},
  year        = {2007},
  volume      = {205},
  number      = {4},
  pages       = {474--511},
}

@inproceedings{hir:mid:zan:08,
  author      = {Hirokawa, N. and Middeldorp, A. and Zankl, H.},
  title       = {Uncurrying for Termination},
  booktitle   = {Proceedings of the 15th International Conference on Logic for Programming, Artifical Intelligence and Reasoning (LPAR '08)},
  year        = {2008},
  editor      = {Cervesato, I. and Veith, H. and Voronkov, A.},
  series      = {LNAI},
  volume      = {5330},
  pages       = {667--681},
  publisher   = {Springer},
}

@article{hon:jak:98,
  author      = {Hong, H. and Jaku{\v{s}}, D.}, 
  title       = {Testing Positiveness of Polynomials},
  journal     = {Journal of Automated Reasoning},
  year        = {1998},
  volume      = {21},
  number      = {1},
  pages       = {23--38},
}

@inproceedings{hon:pfe:99,
  author      = {Hongwei, X. and Pfenning, F.},
  title       = {Dependent types in practical programming},
  booktitle   = {Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages (POPL '99)},
  year        = {1999},
  editor      = {Appel, A. and Aiken, A.},
  pages       = {214--227},
  publisher   = {ACM},
}

@incollection{hue:opp:80,
  author      = {Huet, G. and Oppen, D.C.},
  title       = {Equations and rewrite rules: a survey},
  booktitle   = {Formal Language Theory: Perspectives and Open Problems},
  publisher   = {Academic Press},
  year        = {1980},
  editor      = {Book, R.V.},
  pages       = {349--405},
}

@inproceedings{hug:par:sab:96,
  author      = {Hughes, J. and Pareto, L. and Sabry, A.},
  title       = {Proving the correctness of reactive systems using sized types},
  booktitle   = {Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of programming languages (POPL '96)},
  year        = {1996},
  editor      = {Boehm, H. and Steele, G.},
  pages       = {410--423},
  publisher   = {ACM},
}

@inproceedings{jou:oka:91,
  author      = {Jouannaud, J. and Okada, M.},
  title       = {A computation model for executable higher-order algebraic specification languages},
  booktitle   = {Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science (LICS '91)},
  year        = {1991},
  editor      = {Kahn, G.},
  pages       = {350--361},
  publisher   = {IEEE},
}

@article{jou:oka:97,
  author      = {Jouannaud, J. and Okada, M.},
  title       = {Abstract Data Type Systems},
  journal     = {Theoretical Computer Science},
  year        = {1997},
  volume      = {173},
  number      = {2},
  pages       = {349--391}
}

@inproceedings{jou:rub:99,
  author      = {Jouannaud, J. and Rubio, A.},
  title       = {The higher-order recursive path ordering},
  booktitle   = {Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS '99)},
  year        = {1999},
  series      = {IEEE},
  pages       = {402--411},
}

@article{jou:rub:07,
  author      = {Jouannaud, J. and Rubio, A.}, 
  title       = {Polymorphic higher-order recursive path orderings},
  journal     = {Journal of the ACM},
  year        = {2007},
  volume      = {54},
  number      = {1},
  pages       = {1--48},
} 

@inproceedings{jou:rub:96,
  author      = {Jouannaud, J. and Rubio, A.},
  title       = {A Recursive Path Ordering for Higher-Order Terms in $\eta$-Long $\beta$-Normal Form},
  booktitle   = {Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA '96)},
  year        = {1996},
  editor      = {Ganzinger, H.},
  volume      = {1103},
  series      = {LNCS},
  pages       = {108--122},
  publisher   = {Springer},
}

@article{kah:95,
  author      = {Kahrs, S.},
  title       = {Confluence of curried term-rewriting systems},
  journal     = {Journal of Symbolic Computation},
  year        = {1995},
  volume      = {19},
  number      = {6},
  pages       = {601--623},
}

@unpublished{kam:lev:80,
  author      = {Kamin, S. and L{\'e}vy, J.-J.},
  title       = {Two generalizations of the recursive path ordering},
  year        = {1980},
  note        = {Unpublished Manuscript, University of Illinois},
}

@article{ken:klo:sle:vri:96,
  author      = {Kennaway, R. and Klop, J.W. and Sleep, M.R. and de Vries, F.J.},
  title       = {Comparing curried and uncurried rewriting},
  journal     = {Journal of Symbolic Computation},
  year        = {1996},
  volume      = {21},
  number      = {1},
  pages       = {15--39},
}

@inproceedings{ket:raa:04,
  author      = {Ketema, J. and Raamsdonk, F. van},
  title       = {Erasure and Termination in Higher-Order Rewriting},
  booktitle   = {Proceedings of WST 2004},
  editor      = {Codish, M. and Middeldorp, A.},
  volume      = {AIB-2004-07},
  series      = {Aachener Informatik-Berichte},
  pages       = {30--33},
  school      = {RWTH Aachen},
  year        = {2004}
}

@inproceedings{kha:90,
  author      = {Khasidashvili, Z.},
  title       = {{E}xpression {R}eduction {S}ystems},
  booktitle   = {Proceedings of I. Vekua Institute of Applied Mathematics},
  year        = {1990},
  editor      = {Rukhaia, K.},
  volume      = {36},
  pages       = {200--220},
}

@techreport{kha:92,
  author      = {Khasidashvili, Z.},
  title       = {The {C}hurch-{R}osser theorem in orthogonal {C}ombinatory {R}eduction {S}ystems},
  institution = {{INRIA} Rocqencourt},
  year        = {1992},
  number      = {1825},
}

@article{kha:oos:95,
  author      = {Khasidashvili, Z. and Oostrom, V. van},
  title       = {Context-Sensitive {C}onditional {E}xpression {R}eduction {S}ystems},
  journal     = {Electronic Notes in Theoretical Computer Science},
  year        = {1995},
  volume      = {2},
  pages       = {167--176},
}

@phdthesis{klo:80,
  author      = {Klop, J.W.},
  title       = {{C}ombinatory {R}eduction {S}ystems},
  school      = {CWI Netherlands},
  year        = {1980},
}

@article{klo:oos:raa:93,
  author      = {Klop, J.W. and Oostrom, V. van and Raamsdonk, F. van},
  title       = {Combinatory reduction systems: introduction and survey},
  journal     = {Theoretical Computer Science},
  year        = {1993},
  volume      = {121},
  number      = {1-2},
  pages       = {279 - 308},
}

@unpublished{klo:oos:vri:04,
  author      = {Klop, J.W. and Oostrom, V. van and Vrijer, R. de},
  title       = {Iterative Path Orders},
  year        = {2004},
  note        = {Unpublished Manuscript, Utrecht University and VU University Amsterdam}
}

@inproceedings{klo:oos:vri:06,
  author      = {Klop, J.W. and Oostrom, V. van and Vrijer, R. de},
  title       = {Iterative lexicographic path orders},
  booktitle   = {Essays dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday},
  year        = {2006},
  editor      = {Futatsugi, K. and Jouannaud, J. and Meseguer, J.},
  volume      = {4060},
  series      = {LNCS},
  pages       = {541--554},
  publisher   = {Springer},
  note        = {Festschrift}
}

@inproceedings{kop:11,
  author      = {Kop, C.},
  title       = {Simplifying Algebraic Functional Systems},
  booktitle   = {Proceedings of the 4th International Conference on Algebraic Informatics (CAI '11)},
  year        = {2011},
  editor      = {Winkler, F.},
  volume      = {6742},
  series      = {LNCS},
  pages       = {201--215},
  publisher   = {Springer},
}

@phdthesis{kop:12,
  author      = {Kop, C.},
  title       = {Higher Order Termination},
  school      = {VU University Amsterdam},
  year        = {2012},
}

@inproceedings{kop:raa:08,
  author      = {Kop, C. and Raamsdonk, F. van},
  title       = {A Higher-Order Iterative Path Ordering},
  booktitle   = {Proceedings of the 15th International Conference on Logic for Programming, Artifical Intelligence and Reasoning (LPAR '08)},
  year        = {2008},
  editor      = {Cervesato, I. and Veith, H. and Voronkov, A.},
  volume      = {5330},
  series      = {LNAI},
  pages       = {697--711},
  publisher   = {Springer},
}

@inproceedings{kop:raa:09,
  author      = {Kop, C. and Raamsdonk, F. van},
  title       = {An Iterative Path Ordering},
  booktitle   = {Liber Amicorum for Roel de Vrijer's 60th Birthday},
  year        = {2009},
  editor      = {Klop, J.W. and Oostrom, V. van and Raamsdonk, F.},
  pages       = {145--153},
  note        = {Festschrift}
}

@inproceedings{kop:raa:10,
  author      = {Kop, C. and Raamsdonk, F. van},
  title       = {Higher-order Dependency Pairs with Argument Filterings},
  booktitle   = {Proceedings of the 11th Workshop on Termination (WST '10)},
  year        = {2010},
  note        = {Available at \url{http://hdl.handle.net/1871/33234}}
}

@inproceedings{kop:raa:11,
  author      = {Kop, C. and Raamsdonk, F. van},
  title       = {Higher Order Dependency Pairs for Algebraic Functional Systems},
  booktitle   = {Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11)},
  year        = {2011},
  editor      = {Schmidt-Schau{\ss}, M.},
  volume      = {10},
  series      = {LIPIcs},
  pages       = {203--218},
  publisher   = {Dagstuhl},
}

@article{kop:raa:12,
  author      = {Kop, C. and Raamsdonk, F. van},
  title       = {Dynamic Dependency Pairs for Algebraic Functional Systems},
  journal     = {Logical Methods in Computer Science},
  year        = {2012},
  volume      = {8},
  number      = {2},
  pages       = {10:1--10:51},
  note        = {Included in the Special Issue for RTA '11.}
}

@techreport{kop:06,
  author      = {Koprowski, A.},
  title       = {Coq formalization of the Higher-Order Recursive Path Ordering},
  institution = {Eindhoven University of Technology},
  year        = {2006},
  number      = {CSR-06-21},
}

@article{kop:09,
  author      = {Koprowski, A.},
  title       = {Coq formalization of the higher-order recursive path ordering},
  journal     = {Applicable Algebra in Engineering, Communication and Computing},
  year        = {2009},
  volume      = {20},
  number      = {5},
  pages       = {379-425},
}

@article{kop:wal:09,
  author      = {Koprowski, A. and Waldmann, J.},
  title       = {Max/Plus Tree Automata for Termination of Term Rewriting},
  journal     = {Acta Cybernetica},
  year        = {2009},
  volume      = {19},
  number      = {2},
  pages       = {357--392},
}

@inproceedings{kor:ste:zan:mid:09,
  author      = {Korp, M. and Sternagel, C. and Zankl, H. and Middeldorp, A.}, 
  title       = {{T}yrolean {T}ermination {T}ool 2}, 
  booktitle   = {Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09)},
  year        = {2009},
  editor      = {Treinen, R.},
  volume      = {5595},
  series      = {LNCS},
  pages       = {295--304},
  publisher   = {Springer},
}

@inproceedings{kra:ste:thi:fuh:gie:11,
  author      = {Krauss, A. and Sternagel, C. and Thiemann, R. and Fuhs, C. and Giesl, J.},
  title       = {Termination of {I}sabelle Functions via Termination of Rewriting},
  booktitle   = {Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP '11)},
  year        = {2011},
  editor      = {Eekelen, M. and Geuvers, H. and Schmaltz, J. and Wiedijk, F.},
  volume      = {6898},
  series      = {LNCS},
  pages       = {152--167},
  publisher   = {Springer},
}

@inproceedings{kur:kon:04,
  author      = {Kurihara, M. and Kondo, H.},
  title       = {Efficient {BDD} Encodings for Partial Order Constraints with Application to Expert Systems in Software Verification},
  booktitle   = {Proceedings of the 17th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (IEA/AIE '04)},
  year        = {2004},
  editor      = {Orchard, B. and Yang, C. and Ali, M.},
  volume      = {3029},
  series      = {LNAI},
  pages       = {827--837},
  publisher   = {Springer},
}

@article{kus:01,
  author      = {Kusakari, K.},
  title       = {On proving termination of term rewriting systems 
               with higher-order variables},
  journal     = {IPSJ Transactions on Programming},
  year        = {2001},
  volume      = {42}, 
  number      = {SIG 7 PRO11},
  pages       = {35--45},
}

@article{kus:iso:sak:bla:09,
  author      = {Kusakari, K. and Isogai, Y. and Sakai, M. and Blanqui, F.},
  title       = {Static dependency pair method based on strong computability for higher-order rewrite systems},
  journal     = {IEICE Transactions on Information and Systems},
  year        = {2009},
  volume      = {92},
  number      = {10},
  pages       = {2007--2015},
}

@inproceedings{kus:nak:toy:99,
  author      = {Kusakari, K. and Nakamura, M. and Toyama, Y.},
  title       = {Argument Filtering Transformation},
  booktitle   = {Proceedings of the 1st International {ACM SIGPLAN} Conference on Principles and Practice of Declarative Programming (PPDP '99)},
  year        = {1999},
  editor      = {Nadathur, G.},
  volume      = {1702},
  series      = {LNCS},
  pages       = {47--61},
  publisher   = {Springer},
}

@article{kus:sak:07,
  author      = {Kusakari, K. and Sakai, M.},
  title       = {Enhancing dependency pair method using strong computability in simply-typed term rewriting},
  journal     = {Applicable Algebra in Engineering, Communication and Computing},
  year        = {2007},
  volume      = {18},
  number      = {5},
  pages       = {407--431},
}

@article{kus:sak:09,
  author      = {Kusakari, K. and Sakai, M.},
  title       = {Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques},
  journal     = {IEICE Transactions},
  year        = {2009},
  volume      = {92-D},
  number      = {2},
  pages       = {235--247},
}

@phdthesis{lan:93,
  author      = {Laneve, C.},
  title       = {Optimality and Concurrency in Interaction Systems},
  school      = {Universit\`a di Pisa},
  year        = {1993},
}

@techreport{lan:79,
  author      = {Lankford, D.},
  title       = {On Proving Term Rewriting Systems are {N}oetherian},
  institution = {Louisiana Technical University},
  year        = {1979},
  number      = {MTP-3},
}

@inproceedings{les:83,
  author      = {Lescanne, P.},
  title       = {Computer experiments with the {REVE} term rewriting system generator},
  booktitle   = {Proceedings of the 10th {ACM SIGACT-SIGPLAN} Symposium on Principles of programming languages ({POPL} '83)},
  year        = {1983},
  pages       = {99--108},
  publisher   = {ACM},
}

@phdthesis{lev:78,
  author      = {L\'evy, J.},
  title       = {Reductions correctes et optimales dans le lambda-calcul},
  school      = {Universit\'e de Paris},
  year        = {1978}
}

@phdthesis{lor:93,
  author      = {Lor\'{\i}a-Sa\'{e}nz, C.},
  title       = {A Theoretical Framework for Reasoning about Program Construction based on Extensions of Rewrite Systems},
  school      = {Fachbereich Informatik der Universit\"at Kaiserslautern},
  year        = {1993}
}

@inproceedings{lor:ste:93,
  author      = {Lor\'{\i}a-Sa\'{e}nz, C. and Steinbach, J.},
  title       = {Termination of combined (rewrite and $\lambda$-calculus) systems},
  booktitle   = {Proceedings of the Third International Workshop on Conditional Term Rewriting Systems (CTRS '92)},
  year        = {1993},
  editor      = {Rusinowitch, M. and R\'emy, J.},
  volume      = {656},
  series      = {LNCS},
  pages       = {143--147},
  publisher   = {Springer},
}

@article{luc:05,
  author      = {Lucas, S.},
  title       = {Polynomials over the reals in proofs of termination: from theory to practice},
  journal     = {RAIRO - Theoretical Informatics and Applications},
  year        = {2005},
  volume      = {39},
  number      = {3},
  pages       = {547--586},
}

@inproceedings{lys:pir:95,
  author      = {Lysne, O. and Piris, J.},
  title       = {A termination ordering for higher order rewrite systems},
  booktitle   = {Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA '95)},
  year        = {1995},
  editor      = {Hsiang, J.},
  volume      = {914},
  series      = {LNCS},
  pages       = {26--40},
  publisher   = {Springer},
}

@article{may:nip:98,
  author      = {Mayr, R. and Nipkow, T.},
  title       = {Higher-Order Rewrite Systems and their Confluence},
  journal     = {Theoretical Computer Science},
  year        = {1998},
  volume      = {192},
  number      = {1},
  pages       = {3--29}
}

@phdthesis{mel:96,
  author      = {Melli\`es, P.-A.},
  title       = {Description Abstraite des Syst\`emes de R\'e\'ecriture},
  school      = {Universit\'e Paris VII},
  year        = {1996}
}

@article{mil:91,
  author      = {Miller, D.},
  title       = {A logic programming language with lambda-abstraction, function variables, and simple unification},
  journal     = {Journal of Logic and Computation},
  year        = {1991},
  volume      = {1},
  number      = {4},
  pages       = {497--536}
}

@inproceedings{mol:96,
  author      = {Moller, F.},
  title       = {Infinite results},
  booktitle   = {Proceedings of the 7th International Conference on Concurrency Theory (CONCUR '96)},
  year        = {1996},
  editor      = {Montanari, U. and Sassone, V.},
  volume      = {1119},
  series      = {LNCS},
  pages       = {195--216},
  publisher   = {Springer},
}

@article{nak:nis:kus:sak:sak:10,
  author      = {Nakabayashi, N. and Nishida, N. and Kusakari, K. and Sakabe, T. and Sakai, M.},
  title       = {Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems},
  journal     = {Computer Software},
  volume      = {28},
  number      = {1},
  pages       = {173--189},
  year        = {2010},
  note        = {In Japanese},
}

@inproceedings{nip:91,
  author      = {Nipkow, T.},
  title       = {Higher-order critical pairs},
  booktitle   = {Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science (LICS '91)},
  year        = {1991},
  editor      = {Kahn, G.},
  pages       = {342--349},
  publisher   = {IEEE},
}

@book{ohl:02,
  author      = {Ohlebusch, E.},
  title       = {Advanced Topics in Term Rewriting},
  publisher   = {Springer},
  year        = {2002}
}

@phdthesis{oos:94,
  author      = {Oostrom, V. van},
  title       = {Confluence for abstract and higher-order rewriting},
  school      = {VU University Amsterdam},
  year        = {1994},
}

@inproceedings{oos:97,
  author      = {Oostrom, V. van},
  title       = {Finite family developments},
  booktitle   = {Proceedings of the 8th International Conference on Rewriting Techniques and Applications (RTA '97)},
  year        = {1997},
  editor      = {Comon, H.},
  volume      = 1232,
  series      = {LNCS},
  pages       = {308--322},
  publisher   = {Springer},
}

@inproceedings{oos:raa:93,
  author      = {Oostrom, V. van and Raamsdonk, F.van},
  title       = {Comparing {C}ombinatory {R}eduction {S}ystems and {H}igher-order {R}ewrite {S}ystems},
  booktitle   = {Proceedings of the 1st International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA '93)},
  year        = {1994},
  editor      = {Heering, J. and Meinke, K. and M{\"o}ller, B. and Nipkow, T.},
  volume      = {816},
  series      = {LNCS},
  pages       = {276--304},
  publisher   = {Springer},
}

@inproceedings{ott:bro:ess:gie:10,
  author      = {Otto, C. and Brockschmidt, M. and Essen, C. von and Giesl, J.},
  title       = {Automated Termination Analysis of {J}ava {B}ytecode by Term Rewriting},
  booktitle   = {Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10)},
  year        = {2010},
  editor      = {Lynch, C.},
  volume      = {6},
  series      = {LIPIcs},
  pages       = {259--276},
  publisher   = {Dagstuhl}
}

@inproceedings{pol:93,
  author      = {Pol, J.C. van de},
  title       = {Termination proofs for higher-order rewrite systems},
  booktitle   = {Proceedings of the 1st International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA '93)},
  year        = {1994},
  editor      = {Heering, J. and Meinke, K. and M{\"o}ller, B. and Nipkow, T.},
  volume      = {816},
  series      = {LNCS},
  pages       = {305--325},
  publisher   = {Springer},
}

@inproceedings{pol:94,
  author      = {Pol, J. van},
  title       = {Termination proofs for higher-order rewrite systems},
  booktitle   = {1st International Workshop on Higher-Order Algebra, Logic and Term Rewriting},
  year        = {1994},
  pages       = {305--325},
  publisher   = {Springer}
}

@phdthesis{pol:96,
  author      = {Pol, J.C. van de},
  title       = {Termination of Higher-order Rewrite Systems},
  school      = {University of Utrecht},
  year        = {1996},
}

@inproceedings{pol:sch:95,
  author      = {Pol, J.C. van de and Schwichtenberg, H.},
  title       = {Strict functionals for termination proofs},
  booktitle   = {Proceedings of the 2nd International Conference on Typed Lambda Calculi and Applications (TLCA '95)},
  year        = {1995},
  editor      = {Dezani-Ciancaglini, M. and Plotkin, G.},
  volume      = {902},
  series      = {LNCS},
  pages       = {350--364},
  publisher   = {Springer},
}

@inproceedings{raa:01,
  author      = {Raamsdonk, F. van},
  title       = {On Termination of Higher-Order Rewriting},
  booktitle   = {Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA '01)},
  year        = {2001},
  editor      = {Middeldorp, A.},
  volume      = {2051},
  series      = {LNCS},
  pages       = {261--275},
  publisher   = {Springer},
}

@phdthesis{ros:96,
  author      = {Rose, K.},
  title       = {Combinatory Reduction Systems with Extensions},
  school      = {University of Copenhagen},
  year        = {1996}
}

@inproceedings{ros:11,
  author      = {Rose, K.},
  title       = {{CRSX} - Combinatory Reduction Systems with eXtensions},
  booktitle   = {Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11)},
  year        = {2011},
  editor      = {Schmidt-Schau{\ss}, M.},
  volume      = {10},
  series      = {LIPIcs},
  pages       = {81--90},
  publisher   = {Dagstuhl}
}

@inproceedings{rou:11,
  author      = {Roux, C.},
  title       = {Refinement types as higher-order dependency pairs},
  booktitle   = {Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11)},
  year        = {2011},
  editor      = {Schmidt-Schau{\ss}, M.},
  volume      = {10},
  series      = {LIPIcs},
  pages       = {299--312},
  publisher   = {Dagstuhl},
}

@phdthesis{rou:12,
  author      = {Roux, C.},
  title       = {Terminaison \`a base de tailles: S\'emantique et g\'en\'eralisations},
  school      = {Universit\'e Henri Poincair\'e -- Nancy 1},
  year        = {2012},
}

@article{sak:kus:05,
  author      = {Sakai, M. and Kusakari, K.},
  title       = {On dependency pair method for proving termination of higher-order rewrite systems},
  journal     = {IEICE Transactions on Information and Systems},
  year        = {2005},
  volume      = {E88-D},
  number      = {3},
  pages       = {583--593},
}

@inproceedings{sak:nis:sak:11,
  author      = {Sakata, T. and Nishida, N. and Sakabe, T.},
  title       = {On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs},
  booktitle   = {Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming (WFLP '20)},
  year        = {2011},
  editor      = {Kuchen, H.},
  series      = {LNCS},
  pages       = {138--155},
  publisher   = {Springer},
}

@article{sak:nis:sak:sak:kus:09,
  author      = {Sakata, T. and Nishida, N. and Sakabe, T. and Sakai, M. and Kusakari, K.},
  title       = {Rewriting induction for constrained term rewriting systems},
  journal     = {IPSJ Transactions on Programming},
  volume      = {2},
  number      = {2},
  pages       = {80--96},
  year        = {2009},
  note        = {In Japanese},
}

@article{sak:wat:sak:01,
  author      = {Sakai, M. and Watanabe, Y. and Sakabe, T.},
  title       = {An extension of the dependency pair method for proving termination of higher-order rewrite systems},
  journal     = {IEICE Transactions on Information and Systems},
  year        = {2001},
  volume      = {E84-D},
  number      = {8},
  pages       = {1025--1032},
}

@inproceedings{sch:gie:ser:thi:07,
  author      = {Schneider-Kamp, P. and Giesl, J. and Serebrenik, A. and Thiemann, R.},
  title       = {Automated Termination Analysis for Logic Programs by Term Rewriting},
  booktitle   = {Proceedings of the 16th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR '06)},
  year        = {2007},
  editor      = {Puebla, G.},
  series      = {LNCS},
  volume      = {4407},
  pages       = {177-193},
  publisher   = {Springer},
}

@inproceedings{ste:thi:11,
  author      = {Sternagel, C. and Thiemann, R.},
  title       = {Generalized and Formalized Uncurrying},
  booktitle   = {Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS '11)},
  year        = {2011},
  editor      = {Tinelli, C. and Sofronie-Stokkermans, V.},
  volume      = {6989},
  series      = {LNAI},
  publisher   = {Springer},
  pages       = {243--258},
}

@article{suz:kus:bla:11,
  author      = {Suzuki, S. and Kusakari, K. and Blanqui, F.},
  title       = {Argument Filterings and Usable Rules in Higher-Order Rewrite Systems},
  journal     = {IPSJ Transactions on Programming},
  year        = {2011},
  volume      = {4},
  number      = {2},
  pages       = {1--12},
}

@article{tai:67,
  author      = {Tait, W.},
  title       = {Intensional interpretation of functionals of finite type},
  journal     = {Journal of Symbolic Logic},
  year        = {1967},
  volume      = {32},
  number      = {2},
  pages       = {187--199},
}

@inproceedings{tak:93,
  author      = {Takahashi, M.},
  title       = {$\lambda$-calculi with conditional rules},
  booktitle   = {Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications (TLCA '93)},
  year        = {1993},
  editor      = {Bezem, M. and Groote, J.F.},
  volume      = {664},
  series      = {LNCS},
  pages       = {306--317},
  publisher   = {Springer},
}

@article{tan:gal:91,
  author      = {Tannen, V. and Gallier, G.H.},
  title       = {Polymorphic Rewriting Conserves Algebraic Strong Normalization},
  journal     = {Theoretical Computer Science},
  year        = {1991},
  volume      = {83},
  number      = {1},
  pages       = {3--28}
}

@book{ter:03,
  author      = {Terese},
  title       = {Term Rewriting Systems},
  year        = {2003},
  series      = {Cambridge Tracts in Theoretical Computer Science},
  volume      = {55},
  publisher   = {Cambridge University Press},
}

@phdthesis{thi:07,
  author      = {Thiemann, R.},
  title       = {The {DP} framework for proving termination of term rewriting},
  school      = {RWTH Aachen},
  year        = {2007},
  note        = {Available as Technical Report AIB-2007-17}
}

@inproceedings{thi:all:nag:12,
  author      = {Thiemann, R. and Allais, G. and Nagele, J.},
  title       = {On the Formalization of Termination Techniques based on Multiset Orderings},
  booktitle   = {Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA '12)},
  year        = {2012},
  editor      = {Tiwari, A.},
  volume      = {15},
  series      = {LIPIcs},
  pages       = {339--354},
  publisher   = {Dagstuhl},
}

@inproceedings{thi:ste:09,
  author      = {Thiemann, R. and Sternagel, C.},
  title       = {Certification of Termination Proofs using {CeTA}},
  booktitle   = {Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09)},
  year        = {2009},
  editor      = {Berghofer, S. and Nipkow, T. and Urban, C. and Wenzel, M.},
  volume      = {5674},
  series      = {LNCS},
  pages       = {452--468},
  publisher   = {Springer},
}

@incollection{tse:68,
  author      = {Tseitin, G.},
  title       = {On the Complexity of Derivation in Propositional Calculus},
  booktitle   = {Studies in Constructive Mathematics and Mathematical Logic},
  publisher   = {Nauka, Leningrad},
  year        = {1968},
  pages       = {115--125},
  note        = {Reprinted in Siekmann, J. and Wrightson, G. (editors), \emph{Automation of Reasoning}, 2:466--483, 1983}
}

@article{urb:04,
  author      = {Urbain, X.},
  title       = {Modular and Incremental Automated Termination Proofs},
  journal     = {Journal of Automated Reasoning},
  year        = {2004},
  volume      = {32},
  number      = {4},
  pages       = {315--355},
}

@inproceedings{vid:12,
  author      = {Vidal, G.},
  title       = {Closed symbolic execution for verifying program termination},
  booktitle   = {Proceedings of the 12th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM '12)},
  year        = {2012},
  editor      = {Guerrero, J.},
  volume      = {0},
  pages       = {34--43},
  publisher   = {IEEE},
}

@inproceedings{weh:stu:06,
  author      = {Wehrman, I. and Stump, A.},
  title       = {Mining Propositional Simplification Proofs for Small Validating Clauses},
  booktitle   = {Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '05)},
  year        = {2006},
  editor      = {Armando, A. and Cimatti, A.},
  volume      = {144(2)},
  series      = {ENTCS},
  pages       = {79--91},
  publisher   = {Elsevier},
}

@book{wol:93,
  author      = {Wolfram, D.},
  title       = {The Clausal Theory of Types},
  year        = {1993},
  publisher   = {Cambridge University Press},
  series      = {Cambridge Tracts in Theoretical Computer Science},
  volume      = {21},
}

@article{xi:02,
  author      = {Xi, H.},
  title       = {Dependent Types for Program Termination Verification},
  journal     = {Higher-Order and Symbolic Computation},
  year        = {2002},
  volume      = {15},
  number      = {1},
  pages       = {91--131},
}

@inproceedings{yam:01,
  author      = {Yamada, T.},
  title       = {Confluence and termination of simply typed term rewriting systems},
  booktitle   = {Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA '01)},
  year        = {2001},
  editor      = {Middeldorp, A.},
  volume      = {2051},
  series      = {LNCS}, 
  pages       = {338--352},
  publisher   = {Springer},
}

@article{zan:94,
  author      = {Zantema, H.},
  title       = {Termination of term rewriting: interpretation and type elimination},
  journal     = {Journal of Symbolic Computation},
  year        = {1994},
  volume      = {17},
  pages       = {23--50}
}

@article{zan:95,
  author      = {Zantema, H.},
  title       = {Termination of Term Rewriting by Semantic Labelling},
  journal     = {Fundamenta Informaticae},
  year        = {1995},
  volume      = {24},
  pages       = {89--105},
}

@unpublished{jambox,
  author      = {Endrullis, J.},
  title       = {{Jambox} -- a first-order termination tool},
  note        = {\url{{http://joerg.endrullis.de/}}},
}

@unpublished{satcomp,
  author      = {Community},
  title       = {The international {SAT} Competitions web page},
  note        = {\url{http://www.satcompetition.org/}}
}

@unpublished{smtlib,
  author      = {Community},
  title       = {SMT-LIB},
  note        = {\url{http://www.smtlib.org/}},
}

@unpublished{termcomp,
  author      = {Wiki},
  title       = {{T}ermination {P}ortal},
  note        = {\url{http://www.termination-portal.org/wiki/Termination_Competition}}
}

@unpublished{tpdb,
  author      = {Wiki},
  title       = {{T}ermination {P}roblem {D}ata{B}ase (TPDB)},
  note        = {\url{http://termination-portal.org/wiki/TPDB}}
}

@unpublished{wanda,
  author      = {Kop, C.},
  title       = {{WANDA} -- a higher-order termination tool},
  note        = {\url{http://wandahot.sourceforge.net/}}
}