{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T04:17:37Z","timestamp":1781151457887,"version":"3.54.1"},"reference-count":87,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T00:00:00Z","timestamp":1596412800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EU","award":["RTI2018-094403-B-C32, PROMETEO\/2019\/098, and SP20180225"],"award-info":[{"award-number":["RTI2018-094403-B-C32, PROMETEO\/2019\/098, and SP20180225"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2021,7,31]]},"abstract":"<jats:p>\n            The appropriate selection of the arguments of functions that\n            <jats:italic>can be evaluated<\/jats:italic>\n            in function calls is often useful to improve efficiency, speed, termination behavior, and so on. This is essential, e.g., in the conditional if - then - else operator. We can specify this by associating a set\n            <jats:italic>\u03bc(f)<\/jats:italic>\n            of indices of\n            <jats:italic>evaluable arguments<\/jats:italic>\n            to each function symbol\n            <jats:italic>f<\/jats:italic>\n            . With\n            <jats:italic>\u03bc<\/jats:italic>\n            (if - then - else)={1}, only the Boolean argument\n            <jats:italic>b<\/jats:italic>\n            in calls if\n            <jats:italic>b<\/jats:italic>\n            , then\n            <jats:italic>e<\/jats:italic>\n            else\n            <jats:italic>e'<\/jats:italic>\n            is evaluated. In the realm of term rewriting, this is called\n            <jats:italic>context-sensitive rewriting<\/jats:italic>\n            . It has been proven useful to improve the termination behavior of rewriting computations while it is still able to compute (or approximate) canonical forms like head-normal forms, (infinite) values, and (infinite) normal forms by requiring a few reasonable conditions. This article provides an overview of basic results to use context-sensitive rewriting in practice.\n          <\/jats:p>","DOI":"10.1145\/3397677","type":"journal-article","created":{"date-parts":[[2020,7,7]],"date-time":"2020-07-07T12:38:30Z","timestamp":1594125510000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Context-sensitive Rewriting"],"prefix":"10.1145","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9923-2108","authenticated-orcid":false,"given":"Salvador","family":"Lucas","sequence":"first","affiliation":[{"name":"Valencian Institute of Artificial Intelligence (VRAIN), Universitat Polit\u00e8cnica de Val\u00e8ncia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.03.003"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82529-0"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24537-9_12"},{"key":"e_1_2_1_4_1","volume-title":"Term Rewriting and All That","author":"Baader Franz","unstructured":"Franz Baader and Tobias Nipkow . 1998. Term Rewriting and All That . Cambridge University Press . Franz Baader and Tobias Nipkow. 1998. Term Rewriting and All That. Cambridge University Press."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_27"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45620-1_27"},{"key":"e_1_2_1_8_1","unstructured":"G\u00e9rard Boudol. 1985. Computational semantics of term rewriting systems. Algebr. Methods Semant. (1985) 169--236.  G\u00e9rard Boudol. 1985. Computational semantics of term rewriting systems. Algebr. Methods Semant. (1985) 169--236."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.04.012"},{"key":"e_1_2_1_10_1","volume-title":"Talcott","author":"Clavel Manuel","year":"2015","unstructured":"Manuel Clavel , Francisco Dur\u00e1n , Steven Eker , Santiago Escobar , Patrick Lincoln , Narciso Mart\u00ed-Oliet , and Carolyn L . Talcott . 2015 . Two decades of maude, See Mart\u00ed-Oliet et\u00a0al. [2015], 232--254. DOI:https:\/\/doi.org\/10.1007\/978-3-319-23165-5_11 10.1007\/978-3-319-23165-5_11 Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Mart\u00ed-Oliet, and Carolyn L. Talcott. 2015. Two decades of maude, See Mart\u00ed-Oliet et\u00a0al. [2015], 232--254. DOI:https:\/\/doi.org\/10.1007\/978-3-319-23165-5_11"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"e_1_2_1_12_1","series-title":"Lecture Notes in Computer Science","volume-title":"Talcott","author":"Clavel Manuel","year":"2007","unstructured":"Manuel Clavel , Francisco Dur\u00e1n , Steven Eker , Patrick Lincoln , Narciso Mart\u00ed-Oliet , Jos\u00e9 Meseguer , and Carolyn L . Talcott . 2007 . All About Maude\u2014A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science , Vol. 4350 . Springer . DOI:https:\/\/doi.org\/10.1007\/978-3-540-71999-1 10.1007\/978-3-540-71999-1 Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn L. Talcott. 2007. All About Maude\u2014A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, Vol. 4350. Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00034-9"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"e_1_2_1_15_1","volume-title":"Handbook of Theoretical Computer Science","author":"Courcelle Bruno","unstructured":"Bruno Courcelle . 1990. Recursive applicative program schemes . In Handbook of Theoretical Computer Science , Volume B: Formal Models and Sematics (B). 459-- 492 . Bruno Courcelle. 1990. Recursive applicative program schemes. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B). 459--492."},{"key":"e_1_2_1_16_1","volume-title":"Priestley","author":"Davey Brian A.","year":"1990","unstructured":"Brian A. Davey and Hilary A . Priestley . 1990 . Introduction to Latices and Order. Cambridge University Press . Brian A. Davey and Hilary A. Priestley. 1990. Introduction to Latices and Order. Cambridge University Press."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(79)90071-1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90040-9"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 5th International Workshop on Rewriting Logic and Its Applications (WRLA\u201904)","volume":"117","author":"Dur\u00e1n Francisco","year":"2004","unstructured":"Francisco Dur\u00e1n , Santiago Escobar , and Salvador Lucas . 2004 . New evaluation commands for maude within full maude . In Proceedings of the 5th International Workshop on Rewriting Logic and Its Applications (WRLA\u201904) , Narciso Mart\u00ed-Oliet (ed.), Electronic Notes in Theoretical Computer Science , Vol. 117 . Elsevier, 263--284. DOI:https:\/\/doi.org\/10.1016\/j.entcs.2004.06.014 10.1016\/j.entcs.2004.06.014 Francisco Dur\u00e1n, Santiago Escobar, and Salvador Lucas. 2004. New evaluation commands for maude within full maude. In Proceedings of the 5th International Workshop on Rewriting Logic and Its Applications (WRLA\u201904), Narciso Mart\u00ed-Oliet (ed.), Electronic Notes in Theoretical Computer Science, Vol. 117. Elsevier, 263--284. DOI:https:\/\/doi.org\/10.1016\/j.entcs.2004.06.014"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80019-2"},{"key":"e_1_2_1_21_1","unstructured":"J\u00f6rg\n      Endrullis\n    . 2009. Jambox.\n   (\n  2009\n  ). Retrieved from http:\/\/joerg.endrullis.de\/jambox.html.  J\u00f6rg Endrullis. 2009. Jambox. (2009). Retrieved from http:\/\/joerg.endrullis.de\/jambox.html."},{"key":"e_1_2_1_22_1","volume-title":"Transforming outermost into context-sensitive rewriting. Logic. Methods Comput. Sci. 6, 2","author":"Endrullis J\u00f6rg","year":"2010","unstructured":"J\u00f6rg Endrullis and Dimitri Hendriks . 2010. Transforming outermost into context-sensitive rewriting. Logic. Methods Comput. Sci. 6, 2 ( 2010 ). J\u00f6rg Endrullis and Dimitri Hendriks. 2010. Transforming outermost into context-sensitive rewriting. Logic. Methods Comput. Sci. 6, 2 (2010)."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.03.024"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1062032.1711013"},{"key":"e_1_2_1_25_1","volume-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting Melvin","unstructured":"Melvin Fitting . 1996. First-Order Logic and Automated Theorem Proving ( 2 nd ed.). Springer . DOI:https:\/\/doi.org\/10.1007\/978-1-4612-2360-3 10.1007\/978-1-4612-2360-3 Melvin Fitting. 1996. First-Order Logic and Automated Theorem Proving (2nd ed.). Springer. DOI:https:\/\/doi.org\/10.1007\/978-1-4612-2360-3","edition":"2"},{"key":"e_1_2_1_26_1","volume-title":"Wise","author":"Friedman Daniel P.","year":"1976","unstructured":"Daniel P. Friedman and David S . Wise . 1976 . CONS should not evaluate its arguments. In Proceedings of the 3rd International Colloquium on Automata, Languages and Programming, S. Michaelson and Robin Milner (Eds.). Edinburgh University Press , 257--284. Daniel P. Friedman and David S. Wise. 1976. CONS should not evaluate its arguments. In Proceedings of the 3rd International Colloquium on Automata, Languages and Programming, S. Michaelson and Robin Milner (Eds.). Edinburgh University Press, 257--284."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318610"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICFEM.1997.630424"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006408829523"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004945"},{"key":"#cr-split#-e_1_2_1_31_1.1","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Giesl Albert Rubio Christian Sternagel Johannes Waldmann and Akihisa Yamada. 2019. The termination and complexity competition. In Tools and Algorithms for the Construction and Analysis of Systems-25 Years of TACAS: TOOLympics Held as Part of ETAPS'19 Part III Dirk Beyer Marieke Huisman Fabrice Kordon and Bernhard Steffen (Eds.) Lecture Notes in Computer Science Vol. 11429. Springer 156--166. DOI:https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10 10.1007\/978-3-030-17502-3_10","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"#cr-split#-e_1_2_1_31_1.2","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Giesl Albert Rubio Christian Sternagel Johannes Waldmann and Akihisa Yamada. 2019. The termination and complexity competition. In Tools and Algorithms for the Construction and Analysis of Systems-25 Years of TACAS: TOOLympics Held as Part of ETAPS'19 Part III Dirk Beyer Marieke Huisman Fabrice Kordon and Bernhard Steffen (Eds.) Lecture Notes in Computer Science Vol. 11429. Springer 156--166. DOI:https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR\u201906)","volume":"4130","author":"Giesl J\u00fcrgen","year":"2006","unstructured":"J\u00fcrgen Giesl , Peter Schneider-Kamp , and Ren\u00e9 Thiemann . 2006 a. Automatic termination proofs in the dependency pair framework . In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR\u201906) , Ulrich Furbach and Natarajan Shankar (Eds.), Lecture Notes in Computer Science , Vol. 4130 . Springer, 281--286. DOI:https:\/\/doi.org\/10.1007\/11814771_24 10.1007\/11814771_24 J\u00fcrgen Giesl, Peter Schneider-Kamp, and Ren\u00e9 Thiemann. 2006a. Automatic termination proofs in the dependency pair framework. In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR\u201906), Ulrich Furbach and Natarajan Shankar (Eds.), Lecture Notes in Computer Science, Vol. 4130. Springer, 281--286. DOI:https:\/\/doi.org\/10.1007\/11814771_24"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9057-7"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the Workshop on Graph Reduction, Joseph H","author":"Goguen Joseph A.","unstructured":"Joseph A. Goguen , Claude Kirchner , and Jos\u00e9 Meseguer . 1986. Concurrent term rewriting as a model of computation . In Proceedings of the Workshop on Graph Reduction, Joseph H . Fasel and Robert M. Keller (Eds.), Lecture Notes in Computer Science, Vol. 279 . Springer , 53--93. DOI:https:\/\/doi.org\/10.1007\/3-540-18420-1_50 10.1007\/3-540-18420-1_50 Joseph A. Goguen, Claude Kirchner, and Jos\u00e9 Meseguer. 1986. Concurrent term rewriting as a model of computation. In Proceedings of the Workshop on Graph Reduction, Joseph H. Fasel and Robert M. Keller (Eds.), Lecture Notes in Computer Science, Vol. 279. Springer, 53--93. DOI:https:\/\/doi.org\/10.1007\/3-540-18420-1_50"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6541-0"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/570186.570189"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16310-4_3"},{"key":"#cr-split#-e_1_2_1_39_1.1","doi-asserted-by":"crossref","unstructured":"Ra\u00fal Guti\u00e9rrez and Salvador Lucas. 2015. Function calls at frozen positions in termination of context-sensitive rewriting See Mart\u00ed-Oliet et\u00a0al. [2015] 311--330. DOI:https:\/\/doi.org\/10.1007\/978-3-319-23165-5_15 10.1007\/978-3-319-23165-5_15","DOI":"10.1007\/978-3-319-23165-5_15"},{"key":"#cr-split#-e_1_2_1_39_1.2","doi-asserted-by":"crossref","unstructured":"Ra\u00fal Guti\u00e9rrez and Salvador Lucas. 2015. Function calls at frozen positions in termination of context-sensitive rewriting See Mart\u00ed-Oliet et\u00a0al. [2015] 311--330. DOI:https:\/\/doi.org\/10.1007\/978-3-319-23165-5_15","DOI":"10.1007\/978-3-319-23165-5_15"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_27"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR\u201920)","author":"Guti\u00e9rrez Ra\u00fal","year":"2020","unstructured":"Ra\u00fal Guti\u00e9rrez and Salvador Lucas . 2020 b. MUTERM: Verify termination properties automatically (system description) . In Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR\u201920) , Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.), Lecture Notes in Computer Science. Springer. Ra\u00fal Guti\u00e9rrez and Salvador Lucas. 2020b. MUTERM: Verify termination properties automatically (system description). In Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR\u201920), Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.), Lecture Notes in Computer Science. Springer."},{"key":"e_1_2_1_42_1","volume-title":"Morris","author":"Henderson Peter","year":"1976","unstructured":"Peter Henderson and James H . Morris . 1976 . A lazy evaluator. In Proceedings of the 3rd ACM Symposium on Principles of Programming Languages, Susan L. Graham, Robert M. Graham, Michael A. Harrison, William I. Grosky, and Jeffrey D. Ullman (Eds.). ACM Press , 95--103. DOI:https:\/\/doi.org\/10.1145\/800168.811543 10.1145\/800168.811543 Peter Henderson and James H. Morris. 1976. A lazy evaluator. In Proceedings of the 3rd ACM Symposium on Principles of Programming Languages, Susan L. Graham, Robert M. Graham, Michael A. Harrison, William I. Grosky, and Jeffrey D. Ullman (Eds.). ACM Press, 95--103. DOI:https:\/\/doi.org\/10.1145\/800168.811543"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_18"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_23"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/72551.72554"},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/130697.130699","article-title":"Report on the programming language haskell, A non-strict, purely functional language","volume":"27","author":"Hudak Paul","year":"1992","unstructured":"Paul Hudak , Simon L. Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph H. Fasel , Mar\u00eda M. Guzm\u00e1n , Kevin Hammond , John Hughes , Thomas Johnsson , Richard B. Kieburtz , Rishiyur S. Nikhil , Will Partain , and John Peterson . 1992 . Report on the programming language haskell, A non-strict, purely functional language . SIGPLAN Not. 27 , 5 (1992), 1 . DOI:https:\/\/doi.org\/10.1145\/130697.130699 10.1145\/130697.130699 Paul Hudak, Simon L. Peyton Jones, Philip Wadler, Brian Boutel, Jon Fairbairn, Joseph H. Fasel, Mar\u00eda M. Guzm\u00e1n, Kevin Hammond, John Hughes, Thomas Johnsson, Richard B. Kieburtz, Rishiyur S. Nikhil, Will Partain, and John Peterson. 1992. Report on the programming language haskell, A non-strict, purely functional language. SIGPLAN Not. 27, 5 (1992), 1. DOI:https:\/\/doi.org\/10.1145\/130697.130699","journal-title":"SIGPLAN Not."},{"key":"e_1_2_1_47_1","volume-title":"Huet and Jean-Jacques L\u00e9vy","author":"G\u00e9rard","year":"1991","unstructured":"G\u00e9rard P. Huet and Jean-Jacques L\u00e9vy . 1991 a. Computations in orthogonal rewriting systems, I. In Computational Logic\u2014Essays in Honor of Alan Robinson, Jean-Louis Lassez and Gordon D. Plotkin (Eds.). The MIT Press , 395--414. G\u00e9rard P. Huet and Jean-Jacques L\u00e9vy. 1991a. Computations in orthogonal rewriting systems, I. In Computational Logic\u2014Essays in Honor of Alan Robinson, Jean-Louis Lassez and Gordon D. Plotkin (Eds.). The MIT Press, 395--414."},{"key":"e_1_2_1_48_1","volume-title":"Huet and Jean-Jacques L\u00e9vy","author":"G\u00e9rard","year":"1991","unstructured":"G\u00e9rard P. Huet and Jean-Jacques L\u00e9vy . 1991 b. Computations in orthogonal rewriting systems, II. In Computational Logic\u2014Essays in Honor of Alan Robinson, Jean-Louis Lassez and Gordon D. Plotkin (Eds.). The MIT Press , 415--443. G\u00e9rard P. Huet and Jean-Jacques L\u00e9vy. 1991b. Computations in orthogonal rewriting systems, II. In Computational Logic\u2014Essays in Honor of Alan Robinson, Jean-Louis Lassez and Gordon D. Plotkin (Eds.). The MIT Press, 415--443."},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"J. F. Th.\n      Kamperman\n     and \n      H. R.\n      Walters\n  . \n  1995\n  . Lazy rewriting and eager machinery. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA\u201995) Jieh Hsiang (Ed.) Lecture Notes in Computer Science Vol. \n  914\n  . \n  Springer 147--162. DOI:https:\/\/doi.org\/10.1007\/3-540-59200-8_54    10.1007\/3-540-59200-8_54\nJ. F. Th. Kamperman and H. R. Walters. 1995. Lazy rewriting and eager machinery. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA\u201995) Jieh Hsiang (Ed.) Lecture Notes in Computer Science Vol. 914. Springer 147--162. DOI:https:\/\/doi.org\/10.1007\/3-540-59200-8_54","DOI":"10.1007\/3-540-59200-8_54"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1075"},{"key":"e_1_2_1_51_1","volume-title":"Bendix","author":"Knuth Donald E.","year":"1970","unstructured":"Donald E. Knuth and Peter E . Bendix . 1970 . Simple word problems in universal algebra. In Computational Problems in Abstract Algebra, J. Leech (Ed.). Pergamon Press , 263--297. Donald E. Knuth and Peter E. Bendix. 1970. Simple word problems in universal algebra. In Computational Problems in Abstract Algebra, J. Leech (Ed.). Pergamon Press, 263--297."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70590-1_13"},{"key":"e_1_2_1_53_1","first-page":"802","article-title":"Context-sensitive innermost reachability is decidable for linear right-shallow term rewriting systems","volume":"4","author":"Kojima Yoshiharu","year":"2009","unstructured":"Yoshiharu Kojima , Masahiko Sakai , Naoki Nishida , Keiichirou Kusakari , and Toshiki Sakabe . 2009 . Context-sensitive innermost reachability is decidable for linear right-shallow term rewriting systems . Inf. Media Technol. 4 , 4 (2009), 802 -- 814 . Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe. 2009. Context-sensitive innermost reachability is decidable for linear right-shallow term rewriting systems. Inf. Media Technol. 4, 4 (2009), 802--814.","journal-title":"Inf. Media Technol."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.2197\/ipsjtrans.4.193"},{"key":"e_1_2_1_55_1","volume-title":"Complexity of conditional term rewriting. Logic. Methods Comput. Sci. 13, 1","author":"Kop Cynthia","year":"2017","unstructured":"Cynthia Kop , Aart Middeldorp , and Thomas Sternagel . 2017. Complexity of conditional term rewriting. Logic. Methods Comput. Sci. 13, 1 ( 2017 ). DOI:https:\/\/doi.org\/10.23638\/LMCS-13(1:6)2017 10.23638\/LMCS-13(1:6)2017 Cynthia Kop, Aart Middeldorp, and Thomas Sternagel. 2017. Complexity of conditional term rewriting. Logic. Methods Comput. Sci. 13, 1 (2017). DOI:https:\/\/doi.org\/10.23638\/LMCS-13(1:6)2017"},{"key":"e_1_2_1_57_1","series-title":"Lecture Notes in Computer Science","volume-title":"SOFSEM\u201995, Proceedings of the 22nd Seminar on Current Trends in Theory and Practice of Informatics, Miroslav Bartosek, Jan Staudek, and Jir\u00ed Wiedermann (Eds.)","author":"Lucas Salvador","unstructured":"Salvador Lucas . 1995. Fundamentals of context-sensitive rewriting . In SOFSEM\u201995, Proceedings of the 22nd Seminar on Current Trends in Theory and Practice of Informatics, Miroslav Bartosek, Jan Staudek, and Jir\u00ed Wiedermann (Eds.) , Lecture Notes in Computer Science , Vol. 1012 . Springer , 405--412. DOI:https:\/\/doi.org\/10.1007\/3-540-60609-2_25 10.1007\/3-540-60609-2_25 Salvador Lucas. 1995. Fundamentals of context-sensitive rewriting. In SOFSEM\u201995, Proceedings of the 22nd Seminar on Current Trends in Theory and Practice of Informatics, Miroslav Bartosek, Jan Staudek, and Jir\u00ed Wiedermann (Eds.), Lecture Notes in Computer Science, Vol. 1012. Springer, 405--412. DOI:https:\/\/doi.org\/10.1007\/3-540-60609-2_25"},{"key":"e_1_2_1_58_1","article-title":"Context-sensitive computations in functional and functional logic programs","volume":"1998","author":"Lucas Salvador","year":"1998","unstructured":"Salvador Lucas . 1998 . Context-sensitive computations in functional and functional logic programs . J. Funct. Log. Program. 1998 , 1 (1998). Salvador Lucas. 1998. Context-sensitive computations in functional and functional logic programs. J. Funct. Log. Program. 1998, 1 (1998).","journal-title":"J. Funct. Log. Program."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45127-7_17"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(02)93176-7"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45610-4_21"},{"key":"e_1_2_1_62_1","first-page":"547","article-title":"Polynomials over the reals in proofs of termination: From theory to practice","volume":"39","author":"Lucas Salvador","year":"2005","unstructured":"Salvador Lucas . 2005 . Polynomials over the reals in proofs of termination: From theory to practice . ITA 39 , 3 (2005), 547 -- 586 . DOI:https:\/\/doi.org\/10.1051\/ita:2005029 10.1051\/ita:2005029 Salvador Lucas. 2005. Polynomials over the reals in proofs of termination: From theory to practice. ITA 39, 3 (2005), 547--586. DOI:https:\/\/doi.org\/10.1051\/ita:2005029","journal-title":"ITA"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.07.001"},{"key":"e_1_2_1_64_1","volume-title":"Proving semantic properties as first-order satisfiability. Artif. Intell. 277","author":"Lucas Salvador","year":"2019","unstructured":"Salvador Lucas . 2019. Proving semantic properties as first-order satisfiability. Artif. Intell. 277 ( 2019 ). DOI:https:\/\/doi.org\/10.1016\/j.artint.2019.103174 10.1016\/j.artint.2019.103174 Salvador Lucas. 2019. Proving semantic properties as first-order satisfiability. Artif. Intell. 277 (2019). DOI:https:\/\/doi.org\/10.1016\/j.artint.2019.103174"},{"key":"e_1_2_1_65_1","doi-asserted-by":"crossref","unstructured":"Salvador Lucas. 2020. Applications of context-sensitive rewriting. (submitted).  Salvador Lucas. 2020. Applications of context-sensitive rewriting. (submitted).","DOI":"10.1016\/j.jlamp.2021.100680"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99618"},{"key":"e_1_2_1_67_1","volume-title":"Lecture Notes in Computer Science","volume":"9200","author":"Mart\u00ed-Oliet Narciso","unstructured":"Narciso Mart\u00ed-Oliet , Peter Csaba \u00d6lveczky , and Carolyn L . Talcott (Eds.). 2015. Logic, Rewriting, and Concurrency\u2014Essays dedicated to Jos\u00e9 Meseguer on the Occasion of His 65th Birthday . Lecture Notes in Computer Science , Vol. 9200 . Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-319-23165-5 10.1007\/978-3-319-23165-5 Narciso Mart\u00ed-Oliet, Peter Csaba \u00d6lveczky, and Carolyn L. Talcott (Eds.). 2015. Logic, Rewriting, and Concurrency\u2014Essays dedicated to Jos\u00e9 Meseguer on the Occasion of His 65th Birthday. Lecture Notes in Computer Science, Vol. 9200. Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-319-23165-5"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/367177.367199"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263711"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_24"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12154-3_14"},{"key":"e_1_2_1_73_1","volume-title":"Parallel Languages, Emile H","author":"N\u00f6cker E. G. J. M. H.","year":"1991","unstructured":"E. G. J. M. H. N\u00f6cker , J. E. W. Smetsers , Marko C. J. D. van Eekelen , and Marinus J . Plasmeijer . 1991 . Concurrent clean. In PARLE\u201991: Proceedings of the Parallel Architectures and Languages Europe, Volume II : Parallel Languages, Emile H . L. Aarts, Jan van Leeuwen, and Martin Rem (Eds.), Lecture Notes in Computer Science, Vol. 506. Springer , 202--219. DOI:https:\/\/doi.org\/10.1007\/3-540-54152-7_66 10.1007\/3-540-54152-7_66 E. G. J. M. H. N\u00f6cker, J. E. W. Smetsers, Marko C. J. D. van Eekelen, and Marinus J. Plasmeijer. 1991. Concurrent clean. In PARLE\u201991: Proceedings of the Parallel Architectures and Languages Europe, Volume II: Parallel Languages, Emile H. L. Aarts, Jan van Leeuwen, and Martin Rem (Eds.), Lecture Notes in Computer Science, Vol. 506. Springer, 202--219. DOI:https:\/\/doi.org\/10.1007\/3-540-54152-7_66"},{"key":"e_1_2_1_74_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computing in Systems Described by Equations","author":"O\u2019Donnell Michael J.","unstructured":"Michael J. O\u2019Donnell . 1977. Computing in Systems Described by Equations , Lecture Notes in Computer Science , Vol. 58 . Springer . DOI:https:\/\/doi.org\/10.1007\/3-540-08531-9 10.1007\/3-540-08531-9 Michael J. O\u2019Donnell. 1977. Computing in Systems Described by Equations, Lecture Notes in Computer Science, Vol. 58. Springer. DOI:https:\/\/doi.org\/10.1007\/3-540-08531-9"},{"key":"e_1_2_1_75_1","volume-title":"Advanced Topics in Term Rewriting","author":"Ohlebusch Enno","unstructured":"Enno Ohlebusch . 2002. Advanced Topics in Term Rewriting . Springer . Enno Ohlebusch. 2002. Advanced Topics in Term Rewriting. Springer."},{"key":"e_1_2_1_76_1","unstructured":"Dag Prawitz. 1965. Natural Deduction. A Proof Theoretical Study. Almqvist 8 Wiksell.  Dag Prawitz. 1965. Natural Deduction. A Proof Theoretical Study. Almqvist 8 Wiksell."},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.03.032"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_6"},{"key":"e_1_2_1_79_1","volume-title":"Proceedings of the 24th IFIP WG 1.3 International Workshop on Recent Trends in Algebraic Development Techniques (WADT\u201918)","volume":"11563","author":"Rubio Rub\u00e9n","year":"2018","unstructured":"Rub\u00e9n Rubio , Narciso Mart\u00ed-Oliet , Isabel Pita , and Alberto Verdejo . 2018 . Parameterized strategies specification in maude . In Proceedings of the 24th IFIP WG 1.3 International Workshop on Recent Trends in Algebraic Development Techniques (WADT\u201918) (), Jos\u00e9 Luiz Fiadeiro and Ionut Tutu (Eds.), Lecture Notes in Computer Science , Vol. 11563 . Springer, 27--44. DOI:https:\/\/doi.org\/10.1007\/978-3-030-23220-7_2 10.1007\/978-3-030-23220-7_2 Rub\u00e9n Rubio, Narciso Mart\u00ed-Oliet, Isabel Pita, and Alberto Verdejo. 2018. Parameterized strategies specification in maude. In Proceedings of the 24th IFIP WG 1.3 International Workshop on Recent Trends in Algebraic Development Techniques (WADT\u201918)(), Jos\u00e9 Luiz Fiadeiro and Ionut Tutu (Eds.), Lecture Notes in Computer Science, Vol. 11563. Springer, 27--44. DOI:https:\/\/doi.org\/10.1007\/978-3-030-23220-7_2"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_20"},{"key":"e_1_2_1_81_1","volume-title":"Term Rewriting Systems","unstructured":"Terese. 2003. Term Rewriting Systems . Cambridge Tracts in Theoretical Computer Science, Vol. 55 . Cambridge University Press . Terese. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, Vol. 55. Cambridge University Press."},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_2"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.03.051"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-62950-5_69"},{"key":"e_1_2_1_86_1","volume-title":"Proceedings of the 9th International Workshop on Reduction Strategies in Rewriting and Programming (WRS\u201909)","volume":"15","author":"Zantema Hans","year":"2009","unstructured":"Hans Zantema and Matthias Raffelsieper . 2009 . Stream productivity by outermost termination . In Proceedings of the 9th International Workshop on Reduction Strategies in Rewriting and Programming (WRS\u201909) , Maribel Fern\u00e1ndez (Ed.), EPTCS , Vol. 15 . 83--95. DOI:https:\/\/doi.org\/10.4204\/EPTCS.15.7 10.4204\/EPTCS.15.7 Hans Zantema and Matthias Raffelsieper. 2009. Stream productivity by outermost termination. In Proceedings of the 9th International Workshop on Reduction Strategies in Rewriting and Programming (WRS\u201909), Maribel Fern\u00e1ndez (Ed.), EPTCS, Vol. 15. 83--95. DOI:https:\/\/doi.org\/10.4204\/EPTCS.15.7"},{"key":"e_1_2_1_87_1","volume-title":"Proceedings of the RTA, Christopher Lynch (Ed.), LIPIcs","volume":"6","author":"Zantema Hans","year":"2010","unstructured":"Hans Zantema and Matthias Raffelsieper . 2010 . Proving productivity in infinite data structures . In Proceedings of the RTA, Christopher Lynch (Ed.), LIPIcs , Vol. 6 . Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 401--416. Hans Zantema and Matthias Raffelsieper. 2010. Proving productivity in infinite data structures. In Proceedings of the RTA, Christopher Lynch (Ed.), LIPIcs, Vol. 6. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 401--416."}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3397677","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3397677","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:53Z","timestamp":1750199933000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3397677"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,3]]},"references-count":87,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,7,31]]}},"alternative-id":["10.1145\/3397677"],"URL":"https:\/\/doi.org\/10.1145\/3397677","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,3]]},"assertion":[{"value":"2019-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}