{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:26:55Z","timestamp":1745994415111,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572661"},{"type":"electronic","value":"9783031572678"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Logically constrained term rewriting systems (LCTRSs) are a formalism for program analysis with support for data types that are not (co)inductively defined. Only imperative programs have been considered through the lens of LCTRSs so far since LCTRSs were introduced as a first-order formalism. In this paper, we propose logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order generalization of LCTRSs, which suits the needs of representing and analyzing functional programs. We also study the termination problem of LCSTRSs and define a variant of the higher-order recursive path ordering (HORPO) for the newly proposed formalism.<\/jats:p>","DOI":"10.1007\/978-3-031-57267-8_13","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:02:01Z","timestamp":1712246521000},"page":"331-357","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Higher-Order LCTRSs and Their Termination"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3064-2691","authenticated-orcid":false,"given":"Liye","family":"Guo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6337-2544","authenticated-orcid":false,"given":"Cynthia","family":"Kop","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. TCS 236(1\u20132), 133\u2013178 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00207-8","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Dal\u00a0Lago, U., Moser, G.: Analysing the complexity of functional programs: higher-order meets first-order. In: Reppy, J. (ed.) Proc. ICFP. pp. 152\u2013164 (2015). https:\/\/doi.org\/10.1145\/2784731.2784753","DOI":"10.1145\/2784731.2784753"},{"key":"13_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB). https:\/\/smtlib.cs.uiowa.edu"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Waldmann, U., Wand, D.: A lambda-free higher-order recursive path order. In: Esparza, J., Murawski, A.S. (eds.) Proc. FoSSaCS. pp. 461\u2013479 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_27","DOI":"10.1007\/978-3-662-54458-7_27"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Blanqui, F., Jouannaud, J.P., Rubio, A.: HORPO with computability closure: a reconstruction. In: Dershowitz, N., Voronkov, A. (eds.) Proc. LPAR. pp. 138\u2013150 (2007). https:\/\/doi.org\/10.1007\/978-3-540-75560-9_12","DOI":"10.1007\/978-3-540-75560-9_12"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Blanqui, F., Jouannaud, J.P., Rubio, A.: The computability path ordering: the end of a quest. In: Kaminski, M., Martini, S. (eds.) Proc. CSL. pp. 1\u201314 (2008). https:\/\/doi.org\/10.1007\/978-3-540-87531-4_1","DOI":"10.1007\/978-3-540-87531-4_1"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Ciob\u00e2c\u0103, \u015e., Lucanu, D., Buruian\u0103, A.S.: Operationally-based program equivalence proofs using LCTRSs. JLAMP 135, 100894:1\u2013100894:22 (2023). https:\/\/doi.org\/10.1016\/j.jlamp.2023.100894","DOI":"10.1016\/j.jlamp.2023.100894"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Falke, S., Kapur, D.: A term rewriting approach to the automated termination analysis of imperative programs. In: Schmidt, R.A. (ed.) Proc. CADE. pp. 277\u2013293 (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_22","DOI":"10.1007\/978-3-642-02959-2_22"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Falke, S., Kapur, D.: Rewriting induction + linear arithmetic = decision procedure. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Proc. IJCAR. pp. 241\u2013255 (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_20","DOI":"10.1007\/978-3-642-31365-3_20"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Schmidt-Schau\u00df, M. (ed.) Proc. RTA. pp. 41\u201350 (2011). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2011.41","DOI":"10.4230\/LIPIcs.RTA.2011.41"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Fuhs, C., Kop, C.: A static higher-order dependency pair framework. In: Caires, L. (ed.) Proc. ESOP. pp. 752\u2013782 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_27","DOI":"10.1007\/978-3-030-17184-1_27"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Fuhs, C., Kop, C., Nishida, N.: Verifying procedural programs via constrained rewriting induction. ACM TOCL 18(2), 14:1\u201314:50 (2017). https:\/\/doi.org\/10.1145\/3060143","DOI":"10.1145\/3060143"},{"key":"13_CR13","unstructured":"Furuichi, Y., Nishida, N., Sakai, M., Kusakari, K., Sakabe, T.: Approach to procedural-program verification based on implicit induction of constrained term rewriting systems. IPSJ Trans. Program. 1(2), 100\u2013121 (2008), in Japanese"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. JAR 58, 3\u201331 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9388-y","DOI":"10.1007\/s10817-016-9388-y"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM TOPLAS 33(2), 7:1\u20137:39 (2011). https:\/\/doi.org\/10.1145\/1890028.1890030","DOI":"10.1145\/1890028.1890030"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) Proc. LPAR. pp. 301\u2013331 (2005). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_21","DOI":"10.1007\/978-3-540-32275-7_21"},{"key":"13_CR17","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press (1989)"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Hamza, J., Voirol, N., Kun\u010dak, V.: System FR: formalized foundations for the Stainless verifier. PACMPL 3(OOPSLA), 166:1\u2013166:30 (2019). https:\/\/doi.org\/10.1145\/3360592","DOI":"10.1145\/3360592"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Handley, M.A.T., Vazou, N., Hutton, G.: Liquidate your assets: reasoning about resource usage in Liquid Haskell. PACMPL 4(POPL), 24:1\u201324:27 (2019). https:\/\/doi.org\/10.1145\/3371092","DOI":"10.1145\/3371092"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. In: Madhusudan, P., Seshia, S.A. (eds.) Proc. CAV. pp. 781\u2013786 (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_64","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Jouannaud, J.P., Rubio, A.: The higher-order recursive path ordering. In: Longo, G. (ed.) Proc. LICS. pp. 402\u2013411 (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782635","DOI":"10.1109\/LICS.1999.782635"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. TCS 121(1\u20132), 279\u2013308 (1993). https:\/\/doi.org\/10.1016\/0304-3975(93)90091-7","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Kojima, M., Nishida, N.: From starvation freedom to all-path reachability problems in constrained rewriting. In: Hanus, M., Inclezan, D. (eds.) Proc. PADL. pp. 161\u2013179 (2023). https:\/\/doi.org\/10.1007\/978-3-031-24841-2_11","DOI":"10.1007\/978-3-031-24841-2_11"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Kojima, M., Nishida, N.: Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting. JLAMP 135, 100903:1\u2013100903:19 (2023). https:\/\/doi.org\/10.1016\/j.jlamp.2023.100903","DOI":"10.1016\/j.jlamp.2023.100903"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Kop, C.: Termination of LCTRSs. In: Waldmann, J. (ed.) Proc. WST. pp. 59\u201363 (2013). https:\/\/doi.org\/10.48550\/arXiv.1601.03206","DOI":"10.48550\/arXiv.1601.03206"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Kop, C.: WANDA \u2014 a higher order termination tool. In: Ariola, Z.M. (ed.) Proc. FSCD. pp. 36:1\u201336:19 (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.36","DOI":"10.4230\/LIPIcs.FSCD.2020.36"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Kop, C., Nishida, N.: Term rewriting with logical constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) Proc. FroCoS. pp. 343\u2013358 (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_24","DOI":"10.1007\/978-3-642-40885-4_24"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Kop, C., Vale, D.: hezzel\/cora artifact: ESOP2024 release v4 (2024). https:\/\/doi.org\/10.5281\/zenodo.10560907","DOI":"10.5281\/zenodo.10560907"},{"key":"13_CR29","unstructured":"Kusakari, K.: On proving termination of term rewriting systems with higher-order variables. IPSJ Trans. Program. 42(SIG 7), 35\u201345 (2001), http:\/\/id.nii.ac.jp\/1001\/00016864\/"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Nagao, T., Nishida, N.: Rewriting induction for constrained inequalities. SCP 155, 76\u2013102 (2018). https:\/\/doi.org\/10.1016\/j.scico.2017.10.012","DOI":"10.1016\/j.scico.2017.10.012"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Kahn, G. (ed.) Proc. LICS. pp. 342\u2013349 (1991). https:\/\/doi.org\/10.48456\/tr-218","DOI":"10.48456\/tr-218"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"Nishida, N., Winkler, S.: Loop detection by logically constrained term rewriting. In: Piskac, R., R\u00fcmmer, P. (eds.) Proc. VSTTE. pp. 309\u2013321 (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_18","DOI":"10.1007\/978-3-030-03592-1_18"},{"key":"13_CR33","unstructured":"Pareto, L.: Sized types (1998), licentiate thesis. Chalmers University of Technology"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Reddy, U.S.: Term rewriting induction. In: Stickel, M.E. (ed.) Proc. CADE. pp. 162\u2013177 (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_86","DOI":"10.1007\/3-540-52885-7_86"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. JLAP 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.03.012","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"13_CR36","unstructured":"Sakata, T., Nishida, N., Sakabe, T., Sakai, M., Kusakari, K.: Rewriting induction for constrained term rewriting systems. IPSJ Trans. Program. 2(2), 80\u201396 (2009), in Japanese"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Schneider-Kamp, P., Giesl, J., Str\u00f6der, T., Serebrenik, A., Thiemann, R.: Automated termination analysis for logic programs with cut. TPLP 10(4\u20136), 365\u2013381 (2010). https:\/\/doi.org\/10.1017\/S1471068410000165","DOI":"10.1017\/S1471068410000165"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Sch\u00f6pf, J., Middeldorp, A.: Confluence criteria for logically constrained rewrite systems. In: Pientka, B., Tinelli, C. (eds.) Proc. CADE. pp. 474\u2013490 (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_27","DOI":"10.1007\/978-3-031-38499-8_27"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Suzuki, S., Kusakari, K., Blanqui, F.: Argument filterings and usable rules in higher-order rewrite systems. IPSJ Online Trans. 4, 114\u2013125 (2011). https:\/\/doi.org\/10.2197\/ipsjtrans.4.114","DOI":"10.2197\/ipsjtrans.4.114"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. JSL 32(2), 198\u2013212 (1967). https:\/\/doi.org\/10.2307\/2271658","DOI":"10.2307\/2271658"},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"Thiemann, R., Allais, G., Nagele, J.: On the formalization of termination techniques based on multiset orderings. In: Tiwari, A. (ed.) Proc. RTA. pp. 339\u2013354 (2012). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2012.339","DOI":"10.4230\/LIPIcs.RTA.2012.339"},{"key":"13_CR42","doi-asserted-by":"publisher","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Nagoya termination tool. In: Dowek, G. (ed.) Proc. RTA\u2013TLCA. pp. 466\u2013475 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_32","DOI":"10.1007\/978-3-319-08918-8_32"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57267-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:05:32Z","timestamp":1712246732000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57267-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572661","9783031572678"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57267-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this paper.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"72","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also contain 4 artifact report that have not been part of the original submission","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}