{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:33:20Z","timestamp":1774838000651,"version":"3.50.1"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["1298"],"award-info":[{"award-number":["1298"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Gi 274\/5-2"],"award-info":[{"award-number":["Gi 274\/5-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2011,1]]},"abstract":"<jats:p>There are many powerful techniques for automated termination analysis of term rewriting. However, up to now they have hardly been used for real programming languages. We present a new approach which permits the application of existing techniques from term rewriting to prove termination of most functions defined in Haskell programs. In particular, we show how termination techniques for ordinary rewriting can be used to handle those features of Haskell which are missing in term rewriting (e.g., lazy evaluation, polymorphic types, and higher-order functions). We implemented our results in the termination prover AProVE and successfully evaluated them on existing Haskell libraries.<\/jats:p>","DOI":"10.1145\/1890028.1890030","type":"journal-article","created":{"date-parts":[[2011,2,8]],"date-time":"2011-02-08T13:21:01Z","timestamp":1297171261000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Automated termination proofs for haskell by term rewriting"],"prefix":"10.1145","volume":"33","author":[{"given":"J\u00fcrgen","family":"Giesl","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Raffelsieper","sequence":"additional","affiliation":[{"name":"TU Eindhoven, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[{"name":"University of Southern Denmark, Odense, M, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Swiderski","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[{"name":"University of Innsbruck, Innsbruck, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,2,7]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2004015"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_28"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_44"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68863-1_2"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_35"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_2"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1980681.1980683"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792896"},{"key":"e_1_2_2_12_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV'02)","volume":"2034","author":"Col\u00f3n M."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9087-9"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_22"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70590-1_7"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_3"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-004-0162-8"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/647163.717693"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004945"},{"key":"e_1_2_2_22_1","first-page":"301","article-title":"The dependency pair framework: Combining techniques for automated termination proofs. In Proceedings of the International Conference on Logic Programming, Artificial Intelligence and Reasoning (LPAR'04)","volume":"3452","author":"Giesl J.","year":"2005","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11559306_12"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_23"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_24"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9057-7"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108970.1108973"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462179.1462182"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1778180.1778187"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.10.004"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.010"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_46"},{"key":"e_1_2_2_33_1","unstructured":"Jones M. and Peterson J. 1999. The Hugs 98 user manual. http:\/\/www.haskell.org\/hugs\/  Jones M. and Peterson J. 1999. The Hugs 98 user manual. http:\/\/www.haskell.org\/hugs\/"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0002"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_21"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_2_38_1","first-page":"1","article-title":"Context-Sensitive computations in functional and functional logic programs","volume":"1","author":"Lucas S.","year":"1998","journal-title":"J. Funct. Logic Program."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_36"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_2_2_41_1","first-page":"259","article-title":"Automated termination analysis of Java bytecode by term rewriting. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA'10)","volume":"6","author":"Otto C.","year":"2010","journal-title":"LIPIcs"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/647166.717856"},{"key":"e_1_2_2_43_1","unstructured":"Panitz S. E. 1997. Generierung statischer Programminformation zur Kompilierung verz\u00f6gert ausgewerteter funktionaler Programmiersprachen. Ph.D. thesis University of Frankfurt.  Panitz S. E. 1997. Generierung statischer Programminformation zur Kompilierung verz\u00f6gert ausgewerteter funktionaler Programmiersprachen. Ph.D. thesis University of Frankfurt."},{"key":"e_1_2_2_44_1","unstructured":"Peyton Jones S. 2003. Haskell 98 Languages and Libraries: The Revised Report. Cambridge University Press.  Peyton Jones S. 2003. Haskell 98 Languages and Libraries: The Revised Report. Cambridge University Press."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"key":"e_1_2_2_47_1","unstructured":"Raffelsieper M. 2007. Improving efficiency and power of automated termination analysis for Haskell. Diploma thesis RWTH Aachen. http:\/\/aprove.informatik.rwth-aachen.de\/eval\/Haskell\/DA\/Raffelsieper_DA.pdf  Raffelsieper M. 2007. Improving efficiency and power of automated termination analysis for Haskell. Diploma thesis RWTH Aachen. http:\/\/aprove.informatik.rwth-aachen.de\/eval\/Haskell\/DA\/Raffelsieper_DA.pdf"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.03.032"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614433"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000165"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_19"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291165"},{"key":"e_1_2_2_54_1","volume-title":"Proceedings of the International Logic Programming Symposium (ILPS'95)","author":"S\u00f8rensen M. H."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709095"},{"key":"e_1_2_2_56_1","unstructured":"Swiderski S. 2005. Terminierungsanalyse von Haskellprogrammen. Diploma thesis RWTH Aachen. http:\/\/aprove.informatik.rwth-aachen.de\/eval\/Haskell\/DA\/Swiderski_DA.pdf  Swiderski S. 2005. Terminierungsanalyse von Haskellprogrammen. Diploma thesis RWTH Aachen. http:\/\/aprove.informatik.rwth-aachen.de\/eval\/Haskell\/DA\/Swiderski_DA.pdf"},{"key":"e_1_2_2_57_1","first-page":"474","article-title":"Ensuring termination in ESFP","volume":"6","author":"Telford A.","year":"2000","journal-title":"J. Universal Comput. Sci."},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-005-0179-7"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-95891-8_48"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_6"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)90063-9"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"},{"key":"e_1_2_2_64_1","first-page":"181","article-title":"Termination. In Term Rewriting Systems, Terese, Ed. Cambridge University Press","volume":"6","author":"Zantema H.","year":"2003","journal-title":"Chapter"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1890028.1890030","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1890028.1890030","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:59:39Z","timestamp":1750244379000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1890028.1890030"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":64,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1145\/1890028.1890030"],"URL":"https:\/\/doi.org\/10.1145\/1890028.1890030","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1]]},"assertion":[{"value":"2009-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-02-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}