Alarcón, B., Lucas, S., Navarro-Marset, R.: Proving termination with matrix interpretations over the reals. In: Geser, A., Waldmann, J. (eds.). Proceedings of the 10th International Workshop on Termination, WST 2009), HTWK Leipzig, pp. 12–15 (2009a)
Alarcón, B., Lucas, S., Navarro-Marset, R.: Using matrix interpretations over the reals in proofs of termination. In: Lucio, P., Moreno, G., Peña, R. (eds.). Actas de las IX Jornadas de Programación y Lenguajes (PROLE 2009), SISTEDES, pp. 268–2–77 (2009b)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8
[+]
Alarcón, B., Lucas, S., Navarro-Marset, R.: Proving termination with matrix interpretations over the reals. In: Geser, A., Waldmann, J. (eds.). Proceedings of the 10th International Workshop on Termination, WST 2009), HTWK Leipzig, pp. 12–15 (2009a)
Alarcón, B., Lucas, S., Navarro-Marset, R.: Using matrix interpretations over the reals in proofs of termination. In: Lucio, P., Moreno, G., Peña, R. (eds.). Actas de las IX Jornadas de Programación y Lenguajes (PROLE 2009), SISTEDES, pp. 268–2–77 (2009b)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8
Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Tech. Rep. AIB-2001-09, RWTH Aachen, Germany (2001)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)
Barendregt, H.P., van Eekelen, M.C.J.D., Glauert, J.R.W., Kennaway, R., Plasmeijer, M.J., Sleep, M.R.: Term graph rewriting. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.). PARLE (2), Springer, Lecture Notes in Computer Science, vol. 259, pp. 141–158 (1987)
Bonfante, G., Cichon, A., Marion, J., Touzet, H.: Complexity classes and rewrite systems with polynomial interpretation. In: Gottlob, G., Grandjean, E., Seyr, K. (eds.). Computer Science Logic, 12th International Workshop, CSL ’98, Annual Conference of the EACSL, Brno, Czech Republic, August 24–28, 1998, Proceedings, Springer, Lecture Notes in Computer Science, vol. 1584, pp. 372–384, (1998) https://doi.org/10.1007/10703163_25
Bonfante, G., Cichon, A., Marion, J., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Funct. Prog. 11(1), 33–53 (2001)
Cichon, A., Lescanne, P.: Polynomial interpretations and the complexity of algorithms. In: Kapur, D. (ed.). Automated Deduction: CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15–18, 1992, Proceedings, Springer, Lecture Notes in Computer Science, vol. 607, pp. 139–147, (1992) https://doi.org/10.1007/3-540-55602-8_161
Cichon, E.: Termination orderings and complexity characterizations. In: Aczell, S., Wainer (eds.). Proof Theory: a selection of papers from the Leeds Proof Theory Programme, 1990, Cambridge University Press, Lecture Notes in Computer Science, vol. 607, pp. 171–194 (1992)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude: A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350. Springer (2007). https://doi.org/10.1007/978-3-540-71999-1
Contejean, E., Marché, C., Tomás, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34(4), 325–363 (2005). https://doi.org/10.1007/s10817-005-9022-x
Courcelle, B.: Recursive applicative program schemes. In: van Leeuwen, J. (ed.). Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier and MIT Press, pp. 459–492 (1990) https://doi.org/10.1016/b978-0-444-88074-1.50014-7
Dershowitz, N.: A note on simplification orderings. Inf. Process. Lett. 9(5), 212–215 (1979). https://doi.org/10.1016/0020-0190(79)90071-1
Dershowitz, N.: 33 examples of termination. In: Comon, H., Jouannaud, J. (eds.). Term Rewriting, French Spring School of Theoretical Computer Science, Font Romeux, France, May 17–21, 1993, Advanced Course, Springer, Lecture Notes in Computer Science, vol. 909, pp. 16–26, (1993) https://doi.org/10.1007/3-540-59340-3_2
Durán, F., Escobar, S., Lucas, S.: New Evaluation Commands for Maude Within Full Maude. In: Martí-Oliet, N. (ed.). Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications, WRLA 2004, Barcelona, Spain, March 27–28, 2004, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 117, pp. 263–284, (2004) https://doi.org/10.1016/j.entcs.2004.06.014
Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Programming and symbolic computation in Maude. J. Log. Algebra Method Prog. (2020). https://doi.org/10.1016/j.jlamp.2019.100497
Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2–3), 195–220 (2008)
Fasel, J.H., Hudak, P., Jones, S.L.P., Wadler, P.: SIGPLAN notices special issue on the functional programming language haskell. ACM SIGPLAN Not. 27(5), 1 (1992)
Futatsugi, K., Nakagawa, A.T.: An overview of CAFE specification environment: an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In: First IEEE International Conference on Formal Engineering Methods, ICFEM 1997, Hiroshima, Japan, November 12–14, 1997, Proceedings, IEEE Computer Society, pp. 170–182, (1997) https://doi.org/10.1109/ICFEM.1997.630424
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155–203 (2006). https://doi.org/10.1007/s10817-006-9057-7
Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason. 58(1), 3–31 (2017). https://doi.org/10.1007/s10817-016-9388-y
Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.). Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III, Springer, Lecture Notes in Computer Science, vol. 11429, pp. 156–166, (2019) https://doi.org/10.1007/978-3-030-17502-3_10
Goguen, J.A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing obj Software Engineering with OBJ: algebraic specification in action:169–236 (2000)
Gramlich, B., Lucas, S.: Modular termination of context-sensitive rewriting. In: Proceedings of the 4th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, October 6-8, 2002, Pittsburgh, PA, USA (Affiliated with PLI 2002), ACM, pp. 50–61, (2002a) https://doi.org/10.1145/571157.571163
Gramlich, B., Lucas, S.: Simple termination of context-sensitive rewriting. In: Fischer, B., Visser, E. (eds.). Proceedings of the 2002 ACM SIGPLAN Workshop on Rule-Based Programming, Pittsburgh, Pennsylvania, USA, 2002, ACM, pp. 29–42, (2002b) https://doi.org/10.1145/570186.570189
Grzegorczyk, A.: Some classes of recursive functions. J. Symbol. Logic 20(1), 71–72 (1955). https://doi.org/10.2307/2268082
Gutiérrez, R., Lucas, S.: mu-term: Verify termination properties automatically (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.). Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, Springer, Lecture Notes in Computer Science, vol. 12167, pp. 436–447, (2020) https://doi.org/10.1007/978-3-030-51054-1_28
Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.). Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008, Proceedings, Springer, Lecture Notes in Computer Science, vol. 5195, pp. 364–379, (2008) https://doi.org/10.1007/978-3-540-71070-7_32
Hirokawa, N., Moser, G.: Automated complexity analysis based on context-sensitive rewriting. In: Dowek, G. (ed.). Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings, Springer, Lecture Notes in Computer Science, vol. 8560, pp. 257–271, (2014) https://doi.org/10.1007/978-3-319-08918-8_18
Hirokawa, N., Nagele, J., Middeldorp, A.: Cops and CoCoWeb: Infrastructure for Confluence Tools. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.). Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Springer, Lecture Notes in Computer Science, vol. 10900, pp. 346–353, (2018) https://doi.org/10.1007/978-3-319-94205-6_23
Hofbauer, D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theor. Comput. Sci. 105(1), 129–140 (1992). https://doi.org/10.1016/0304-3975(92)90289-R
Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations (preliminary version). In: Dershowitz, N. (ed.). Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, April 3–5, 1989, Proceedings, Springer, Lecture Notes in Computer Science, vol. 355, pp. 167–177, (1989) https://doi.org/10.1007/3-540-51081-8_107
Knuth, D.E., Bendix, P.E.: Simple word problems in universal algebra. In: Leech, J. (ed.). Computational Problems in Abstract Algebra, Pergamon Press, pp. 263–297 (1970)
Lankford, D.S.: On proving term rewriting systems are noetherian. Louisiana Technological University, Ruston, LA, Tech. rep (1979)
Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294–343 (2002a). https://doi.org/10.1006/inco.2002.3176
Lucas, S.: Termination of (canonical) context-sensitive rewriting. In: Tison, S. (ed.). RTA, Springer, Lecture Notes in Computer Science, vol. 2378, pp. 296–310 (2002b)
Lucas, S.: A note on completeness of conditional context-sensitive rewriting. In: 5th International Workshop on Reduction Strategies in Rewriting and Programming, pp. 3–15. University of Kyoto, WRS (2005a)
Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. ITA 39(3), 547–586 (2005b). https://doi.org/10.1051/ita:2005029
Lucas, S.: Context-sensitive rewriting. ACM Comput. Surv. 53(4), 78:1–78:36 (2020). https://doi.org/10.1145/3397677
Lucas, S.: Applications and extensions of context-sensitive rewriting. J. Logical Algebraic Methods Prog. 121, 100680 (2021). https://doi.org/10.1016/j.jlamp.2021.100680
Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science, pp. 789–792 (1970)
McCarthy, J.: Towards a mathematical science of computation. In: Information Processing, Proceedings of the 2nd IFIP Congress 1962, Munich, Germany, August 27–September 1, 1962, North-Holland, pp. 21–28 (1962)
Middeldorp, A.: Call by need computations to root-stable form. In: Lee, P., Henglein, F., Jones, N.D. (eds.). Conference Record of POPL’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15–17 January 1997, ACM Press, pp. 94–105 (1997) https://doi.org/10.1145/263699.263711
Moser, G., Schnabl, A.: The derivational complexity induced by the dependency pair method. Logical Methods Comput. Sci. (2011). https://doi.org/10.2168/LMCS-7(3:1)2011
Moser, G., Schnabl, A., Waldmann, J.: Complexity analysis of term rewriting based on matrix and context dependent interpretations. In: Hariharan, R., Mukund, M., Vinay, V. (eds.). IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, December 9–11, 2008, Bangalore, India, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs, vol. 2, pp. 304–315 (2008). https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1762
Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewriting. In: Schmidt-Schauß, M. (ed.). Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30–June 1, 2011, Novi Sad, Serbia, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs, vol. 10, pp. 251–266 (2011), https://doi.org/10.4230/LIPIcs.RTA.2011.251
Neurauter, F., Zankl, H., Middeldorp, A.: Revisiting matrix interpretations for polynomial derivational complexity of term rewriting. In: Fermüller, C.G., Voronkov, A. (eds.). Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings, Springer, Lecture Notes in Computer Science, vol. 6397, pp. 550–564 (2010), https://doi.org/10.1007/978-3-642-16242-8_39
Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reason. 51(1), 27–56 (2013). https://doi.org/10.1007/s10817-013-9277-6
Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer (2002)
Péchoux, R.: Synthesis of sup-interpretations: a survey. Theor. Comput. Sci. 467, 30–52 (2013). https://doi.org/10.1016/j.tcs.2012.11.003
Rapp, F., Middeldorp, A.: FORT 2.0. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.). Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Springer, Lecture Notes in Computer Science, vol. 10900, pp. 81–88 (2018), https://doi.org/10.1007/978-3-319-94205-6_6
Ritchie, R.W.: Classes of predictably computable functions. Trans. Am. Math. Soc. 106, 139–173 (1963)
Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A.: Parameterized Strategies Specification in Maude. In: Fiadeiro, J.L., Tutu, I. (eds.). Recent Trends in Algebraic Development Techniques: 24th IFIP WG 1.3 International Workshop, WADT 2018, Egham, UK, July 2-5, 2018, Revised Selected Papers, Springer, Lecture Notes in Computer Science, vol. 11563, pp. 27–44 (2018), https://doi.org/10.1007/978-3-030-23220-7_2
Steinbach, J.: Proving polynomials positive. In: Shyamasundar, R.K. (ed.). Foundations of Software Technology and Theoretical Computer Science, 12th Conference, New Delhi, India, December 18–20, 1992, Proceedings, Springer, Lecture Notes in Computer Science, vol. 652, pp. 191–202 (1992), https://doi.org/10.1007/3-540-56287-7_105
Sternagel, C., Thiemann, R.: Signature extensions preserve termination: an alternative proof via dependency pairs. In: Dawar, A., Veith, H. (eds.). Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23–27, 2010. Proceedings, Springer, Lecture Notes in Computer Science, vol. 6247, pp. 514–528 (2010), https://doi.org/10.1007/978-3-642-15205-4_39
Terese.: Term Rewriting Systems, Cambridge tracts in theoretical computer science, vol. 55. Cambridge University Press (2003)
Waldmann, J.: Polynomially bounded matrix interpretations. In: Lynch, C. (ed.). Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11–13, 2010, Edinburgh, Scottland, UK, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs, vol. 6, pp. 357–372 (2010), https://doi.org/10.4230/LIPIcs.RTA.2010.357
Weiermann, A.: Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths. Theor. Comput.Sci. 139(1 & 2), 355–362 (1995). https://doi.org/10.1016/0304-3975(94)00135-6
Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17(1), 23–50 (1994). https://doi.org/10.1006/jsco.1994.1003
Zantema, H.: Termination of context-sensitive rewriting. In: Comon, H. (ed.). Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2–5, 1997, Proceedings, Springer, Lecture Notes in Computer Science, vol. 1232, pp. 172–186 (1997), https://doi.org/10.1007/3-540-62950-5_69
[-]
