{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:38Z","timestamp":1775790698317,"version":"3.50.1"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-2006535, CNS-2244494"],"award-info":[{"award-number":["CCF-2006535, CNS-2244494"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,8,15]]},"abstract":"<jats:p>Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computation cost. Existing works either require manually annotating sharing, or rely on separation logic to reason about heaps of mutable cells. In this paper, we propose a bidirectional demand semantics that allows for extrinsic reasoning about the computation cost of lazy programs without relying on special program logics. To show the effectiveness of our approach, we apply the demand semantics to a variety of case studies including insertion sort, selection sort, Okasaki\u2019s banker\u2019s queue, and the implicit queue. We formally prove that the banker\u2019s queue and the implicit queue are both amortized and persistent using the Rocq Prover (formerly known as Coq). We also propose the reverse physicist\u2019s method, a novel variant of the classical physicist\u2019s method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics.<\/jats:p>","DOI":"10.1145\/3674626","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"30-63","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Story of Your Lazy Function\u2019s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2673-4400","authenticated-orcid":false,"given":"Li-yao","family":"Xia","sequence":"first","affiliation":[{"name":"Unaffiliated, Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5008-1785","authenticated-orcid":false,"given":"Laura","family":"Israel","sequence":"additional","affiliation":[{"name":"Portland State University, Portland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0623-2293","authenticated-orcid":false,"given":"Maite","family":"Kramarz","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4832-7016","authenticated-orcid":false,"given":"Nicholas","family":"Coltharp","sequence":"additional","affiliation":[{"name":"Portland State University, Portland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8113-4478","authenticated-orcid":false,"given":"Koen","family":"Claessen","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-9168","authenticated-orcid":false,"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8720-883X","authenticated-orcid":false,"given":"Yao","family":"Li","sequence":"additional","affiliation":[{"name":"Portland State University, Portland, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_1_2_1","article-title":"Electronic textbook. Version 1.5.4","author":"Appel Andrew W.","year":"2023","unstructured":"Andrew W. Appel, Andrew Tolmach, and Michael Clarkson. 2023. Verified Functional Algorithms. Electronic textbook. Version 1.5.4. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf.","journal-title":"Verified Functional Algorithms"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_3_1_4_1","unstructured":"Fr\u00e9d\u00e9ric Besson and Evgeny Makarov. 2023. Micromega: solvers for arithmetic goals over ordered rings. https:\/\/coq.inria.fr\/doc\/v8.17\/refman\/addendum\/micromega.html"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99382"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000283"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409026"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408979"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428123"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581487"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944731"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3310340"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236797"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_13"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.20"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_11"},{"key":"e_1_3_1_19_1","article-title":"Amortized Analysis via Coinduction","author":"Grodin Harrison","year":"2023","unstructured":"Harrison Grodin and Robert Harper. 2023. Amortized Analysis via Coinduction. CoRR abs\/2303.16048 (2023). arXiv:2303.16048 https:\/\/arxiv.org\/abs\/2303.16048","journal-title":"CoRR"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507667"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341718"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005769"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/222124.222146"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.2.98"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3236-3_17"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/225058.225090"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_3_1_31_1","unstructured":"Paul Blain Levy . 2001. Call-by-push-value. Ph. D. Dissertation. Queen Mary University of London UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.369233"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473585"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2017.05.001"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292547"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498670"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/580840"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408984"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632892"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434308"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227716"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263760"},{"key":"e_1_3_1_46_1","unstructured":"Ilya Sergey Simon Peyton Jones and Dimitrios Vytiniotis. 2014. Theory and practice of demand analysis in Haskell. https:\/\/www.microsoft.com\/en-us\/research\/publication\/theory-practice-demand-analysis-haskell\/ Unpublished draft."},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000016"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_3_1_50_1","unstructured":"Niki Vazou . 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph. D. Dissertation. University of California San Diego USA. http:\/\/www.escholarship.org\/uc\/item\/8dm057ws"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18317-5_21"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"Li-yao Xia Laura Israel Maite Kramarz Nicholas Coltharp Koen Claessen Stephanie Weirich and Yao Li. 2024. Story of Your Lazy Functions Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs (Artifact). https:\/\/doi.org\/10.5281\/zenodo.11493754 10.5281\/zenodo.11493754","DOI":"10.5281\/zenodo.11493754"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674626","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674626","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:49:29Z","timestamp":1770191369000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674626"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":51,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674626"],"URL":"https:\/\/doi.org\/10.1145\/3674626","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}