{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:10:01Z","timestamp":1748581801610,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319231648"},{"type":"electronic","value":"9783319231655"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23165-5_15","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T03:57:43Z","timestamp":1440561463000},"page":"311-330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting"],"prefix":"10.1007","author":[{"given":"Ra\u00fal","family":"Guti\u00e9rrez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salvador","family":"Lucas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"636","DOI":"10.1007\/978-3-540-89439-1_44","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B Alarc\u00f3n","year":"2008","unstructured":"Alarc\u00f3n, B., Emmes, F., Fuhs, C., Giesl, J., Guti\u00e9rrez, R., Lucas, S., Schneider-Kamp, P., Thiemann, R.: Improving context-sensitive dependency pairs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 636\u2013651. Springer, Heidelberg (2008)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/11944836_28","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"B Alarc\u00f3n","year":"2006","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S.: Context-sensitive dependency pairs. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 297\u2013308. Springer, Heidelberg (2006)"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"922","DOI":"10.1016\/j.ic.2010.03.003","volume":"208","author":"B Alarc\u00f3n","year":"2010","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S.: Context-Sensitive dependency pairs. Inf. Comput. 208, 922\u2013968 (2010)","journal-title":"Inf. Comput."},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-17796-5_12","volume-title":"Algebraic Methodology and Software Technology","author":"B Alarc\u00f3n","year":"2011","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201\u2013208. Springer, Heidelberg (2011)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-62950-5_68","volume-title":"Rewriting Techniques and Applications","author":"T Arts","year":"1997","unstructured":"Arts, T., Giesl, J.: Proving innermost normalisation automatically. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 151\u2013171. Springer, Heidelberg (1997)"},{"issue":"1\u20132","key":"15_CR6","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1\u20132), 133\u2013178 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/S1571-0661(05)82552-6","volume":"15","author":"P Borovansk\u00fd","year":"1998","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner, H., Moreau, P., Ringeissen, C.: An overview of ELAN. Electr. Notes Theor. Comput. Sci. 15, 55\u201370 (1998). http:\/\/dx.doi.org\/10.1016\/S15710661(05)825526","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"15_CR10","unstructured":"Emmes, F.: Automated Termination Analysis of Context-Sensitive Term Rewrite Systems. Master\u2019s thesis, Fakult\u00e4t f\u00fcr Mathematik, Informatik und Naturwissenschaften der Rheinisch-Westf\u00e4lischen Technischen Hochschule Aachen, Aachen, Germany (2008)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Goguen, J.A., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1985, pp. 52\u201366. ACM (1985)","DOI":"10.1145\/318593.318610"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Nakagawa, A.: An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In: Proceedings of the 1st International Conference on Formal Engineering Methods, ICFEM 1997, p. 170. IEEE Computer Society (1997)","DOI":"10.1109\/ICFEM.1997.630424"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-45005-X_20","volume-title":"Developments in Language Theory","author":"J Giesl","year":"2003","unstructured":"Giesl, J., Middeldorp, A.: Innermost termination of context-sensitive rewriting. In: Ito, M., Toyama, M. (eds.) DLT 2002. LNCS, vol. 2450, pp. 231\u2013244. Springer, Heidelberg (2003)"},{"issue":"3","key":"15_CR14","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reasoning 37(3), 155\u2013203 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"15_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6541-0","volume-title":"Software Engineering with OBJ: Algebraic Specification in Action","author":"JA Goguen","year":"2000","unstructured":"Goguen, J.A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Software Engineering with OBJ: Algebraic Specification in Action. Kluwer, Boston (2000). chap. Introducing OBJ"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/BF01190827","volume":"5","author":"B Gramlich","year":"1994","unstructured":"Gramlich, B.: Generalized sufficient conditions for modular termination of rewriting. Appl. Algebra Eng. Commun. Comput. 5, 131\u2013151 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-16310-4_3","volume-title":"Rewriting Logic and Its Applications","author":"R Guti\u00e9rrez","year":"2010","unstructured":"Guti\u00e9rrez, R., Lucas, S.: Proving termination in the context-sensitive dependency pair framework. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 18\u201334. Springer, Heidelberg (2010)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Guti\u00e9rrez, R., Lucas, S.: Function calls at frozen positions in termination of context-sensitive rewriting. Technical report, DSIC, Universitat Polit\u00e8cnica de Val\u00e8ncia, May 2015. http:\/\/hdl.handle.net\/10251\/50750","DOI":"10.1007\/978-3-319-23165-5_15"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-70590-1_9","volume-title":"Rewriting Techniques and Applications","author":"R Guti\u00e9rrez","year":"2008","unstructured":"Guti\u00e9rrez, R., Lucas, S., Urbain, X.: Usable rules for context-sensitive rewrite systems. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 126\u2013141. Springer, Heidelberg (2008)"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-73449-9_18","volume-title":"Term Rewriting and Applications","author":"J Hendrix","year":"2007","unstructured":"Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 229\u2013245. Springer, Heidelberg (2007)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-25979-4_18","volume-title":"Rewriting Techniques and Applications","author":"N Hirokawa","year":"2004","unstructured":"Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249\u2013268. Springer, Heidelberg (2004)"},{"issue":"4","key":"15_CR22","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1016\/j.ic.2006.08.010","volume":"205","author":"N Hirokawa","year":"2007","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: techniques and features. Inf. Comput. 205(4), 474\u2013511 (2007)","journal-title":"Inf. Comput."},{"issue":"1","key":"15_CR23","first-page":"1","volume":"1998","author":"S Lucas","year":"1998","unstructured":"Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Funct. Logic Program. 1998(1), 1\u201361 (1998)","journal-title":"J. Funct. Logic Program."},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Lucas, S.: Termination of on-demand rewriting and termination of OBJ programs. In: De Nicola, R., S\u00f8ndergaard, H. (eds.) Proceedings of the 3rd Internatinal Conference on Principles and Practice of Declarative Programming, PPDP 2001, pp. 82\u201393. ACM Press (2001)","DOI":"10.1145\/773184.773194"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","first-page":"666","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Lucas","year":"2001","unstructured":"Lucas, S.: Termination of rewriting with strategy annotations. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 666\u2013680. Springer, Heidelberg (2001)"},{"issue":"3","key":"15_CR26","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1051\/ita:2005029","volume":"39","author":"S Lucas","year":"2005","unstructured":"Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theor. Inf. Appl. 39(3), 547\u2013586 (2005)","journal-title":"RAIRO Theor. Inf. Appl."},{"issue":"2","key":"15_CR27","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.ipl.2014.07.004","volume":"115","author":"S Lucas","year":"2015","unstructured":"Lucas, S.: Completeness of context-sensitive rewriting. Inf. Process. Lett. 115(2), 87\u201392 (2015). http:\/\/dx.doi.org\/10.1016\/j.ipl.2014.07.004","journal-title":"Inf. Process. Lett."},{"key":"15_CR28","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(94)00039-L","volume":"136","author":"E Ohlebusch","year":"1994","unstructured":"Ohlebusch, E.: On the modularity of termination of term rewriting systems. Theor. Comput. Sci. 136, 333\u2013360 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-62950-5_69","volume-title":"Rewriting Techniques and Applications","author":"H Zantema","year":"1997","unstructured":"Zantema, H.: Termination of context-sensitive rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Logic, Rewriting, and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23165-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T04:39:45Z","timestamp":1748579985000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23165-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319231648","9783319231655"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23165-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}