{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:21:29Z","timestamp":1750306889278,"version":"3.41.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"9","license":[{"start":{"date-parts":[[2012,9,9]],"date-time":"2012-09-09T00:00:00Z","timestamp":1347148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGPLAN Not."],"published-print":{"date-parts":[[2012,10,15]]},"abstract":"<jats:p>\n            This paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and Jost, which was previously restricted to eager evaluation. In this paper, we extend this work to a lazy setting by capturing the costs of unevaluated expressions in type annotations and by amortising the payment of these costs using a notion of\n            <jats:italic>lazy potential<\/jats:italic>\n            . We present our analysis as a proof system for predicting heap allocations of a minimal functional language (including higher-order functions and recursive data types) and define a formal cost model based on Launchbury's natural semantics for lazy evaluation. We prove the soundness of our analysis with respect to the cost model. Our approach is illustrated by a number of representative and non-trivial examples that have been analysed using a prototype implementation of our analysis.\n          <\/jats:p>","DOI":"10.1145\/2398856.2364575","type":"journal-article","created":{"date-parts":[[2012,11,20]],"date-time":"2012-11-20T15:50:20Z","timestamp":1353426620000},"page":"165-176","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Automatic amortised analysis of dynamic memory allocation for lazy functional programs"],"prefix":"10.1145","volume":"47","author":[{"given":"Hugo","family":"Sim\u00f5es","sequence":"first","affiliation":[{"name":"Universidade do Porto, Porto, Portugal"}]},{"given":"Pedro","family":"Vasconcelos","sequence":"additional","affiliation":[{"name":"Universidade do Porto, Porto, Portugal"}]},{"given":"M\u00e1rio","family":"Florido","sequence":"additional","affiliation":[{"name":"Universidade do Porto, Porto, Portugal"}]},{"given":"Steffen","family":"Jost","sequence":"additional","affiliation":[{"name":"Ludwig Maximillians Universit\u00e4t, Munich, Germany"}]},{"given":"Kevin","family":"Hammond","sequence":"additional","affiliation":[{"name":"University of St Andrews, St Andrews, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2012,9,9]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"13","volume-title":"Proc. AGP-2003:  2003 Joint Conf. on Declarative Prog.","author":"Albert E.","year":"2003","unstructured":"E. Albert , J. Silva , and G. Vidal . Time Equations for Lazy Functional (Logic) Languages . In Proc. AGP-2003: 2003 Joint Conf. on Declarative Prog. , Reggio Calabria, Italy , Sept. 3-5, 2003 , pages 13 -- 24 , 2003. E. Albert, J. Silva, and G. Vidal. Time Equations for Lazy Functional (Logic) Languages. In Proc. AGP-2003: 2003 Joint Conf. on Declarative Prog., Reggio Calabria, Italy, Sept. 3-5, 2003, pages 13--24, 2003."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542431.1542450"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806651.1806671"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002724"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/351268.351287"},{"key":"e_1_2_1_6_1","volume-title":"A Space Semantics for Core Haskell. Electr. Notes Theor. Comput. Sci., 41(1)","author":"Bakewell A.","year":"2000","unstructured":"A. Bakewell and C. Runciman . A Space Semantics for Core Haskell. Electr. Notes Theor. Comput. Sci., 41(1) , 2000 . A. Bakewell and C. Runciman. A Space Semantics for Core Haskell. Electr. Notes Theor. Comput. Sci., 41(1), 2000."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99382"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375634.1375655"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_14"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375634.1375656"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_1_13_1","first-page":"88","volume-title":"Proc. IFL '01: Impl. of Functional Langs.","author":"de la Encina A.","year":"2001","unstructured":"A. de la Encina and R. Pe\u00f1a-Mar\u00ed . Proving the Correctness of the STG Machine . In Proc. IFL '01: Impl. of Functional Langs. , Stockholm, Sweden, Sept . 24-26, 2001 , pages 88 -- 104 . Springer LNCS 2312, 2002. A. de la Encina and R. Pe\u00f1a-Mar\u00ed. Proving the Correctness of the STG Machine. In Proc. IFL '01: Impl. of Functional Langs., Stockholm, Sweden, Sept. 24-26, 2001, pages 88--104. Springer LNCS 2312, 2002."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888262"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006746"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102805"},{"key":"e_1_2_1_17_1","first-page":"26","author":"Gustavsson J.","year":"1999","unstructured":"J. Gustavsson and D. Sands . A Foundation for Space-Safe Transformations of Call-by-Need Programs. Electronic Notes on Theoretical Computer Science , 26 , 1999 . J. Gustavsson and D. Sands. A Foundation for Space-Safe Transformations of Call-by-Need Programs. Electronic Notes on Theoretical Computer Science, 26, 1999.","journal-title":"A Foundation for Space-Safe Transformations of Call-by-Need Programs. Electronic Notes on Theoretical Computer Science"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_3"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1807662.1807689"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.2.98"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000319"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90122-9"},{"key":"e_1_2_1_26_1","volume-title":"Dipl. Thesis, Darmstadt Univ. of Tech.","author":"Jost S.","year":"2002","unstructured":"S. Jost . Static Prediction of Dynamic Space Usage of Linear Functional Programs , Dipl. Thesis, Darmstadt Univ. of Tech. , 2002 . S. Jost. Static Prediction of Dynamic Space Usage of Linear Functional Programs, Dipl. Thesis, Darmstadt Univ. of Tech., 2002."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003037"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292547"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289439"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/280586"},{"key":"e_1_2_1_36_1","volume-title":"Yale University","author":"S. Peyton Jones","year":"1999","unstructured":"S. Peyton Jones (ed.), L. Augustsson , B. Boutel , F. Burton , J. Fasel , A. Gordon , K. Hammond , R. Hughes , P. Hudak , T. Johnsson , M. Jones , J. Peterson , A. Reid , and P. Wadler . Report on the Non-Strict Functional Language, Haskell (Haskell98). Technical report , Yale University , 1999 . S. Peyton Jones (ed.), L. Augustsson, B. Boutel, F. Burton, J. Fasel, A. Gordon, K. Hammond, R. Hughes, P. Hudak, T. Johnsson, M. Jones, J. Peterson, A. Reid, and P. Wadler. Report on the Non-Strict Functional Language, Haskell (Haskell98). Technical report, Yale University, 1999."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/92011.92040"},{"key":"e_1_2_1_38_1","unstructured":"D. Sands. Calculi for Time Analysis of Functional Programs. PhD thesis Imperial College University of London September 1990.  D. Sands. Calculi for Time Analysis of Functional Programs. PhD thesis Imperial College University of London September 1990."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80694-2"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002712"},{"key":"e_1_2_1_41_1","first-page":"351","volume-title":"Eekelen. Polynomial Size Analysis of First-Order Functions. In Proc. TLCA 2007: Typed Lambda Calculi and Applications (TLCA 2007","author":"Shkaravska O.","year":"2007","unstructured":"O. Shkaravska , R. van Kesteren , and M. van Eekelen. Polynomial Size Analysis of First-Order Functions. In Proc. TLCA 2007: Typed Lambda Calculi and Applications (TLCA 2007 ), pages 351 -- 365 , Paris, France , June 26-28, June 2007 . Springer LNCS 4583. O. Shkaravska, R. van Kesteren, and M. van Eekelen. Polynomial Size Analysis of First-Order Functions. In Proc. TLCA 2007: Typed Lambda Calculi and Applications (TLCA 2007), pages 351--365, Paris, France, June 26-28, June 2007. Springer LNCS 4583."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27861-0_6"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73571"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/36583.36604"}],"container-title":["ACM SIGPLAN Notices"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2398856.2364575","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2398856.2364575","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:48Z","timestamp":1750234728000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2398856.2364575"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9,9]]},"references-count":43,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2012,10,15]]}},"alternative-id":["10.1145\/2398856.2364575"],"URL":"https:\/\/doi.org\/10.1145\/2398856.2364575","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2364527.2364575","asserted-by":"subject"}]},"ISSN":["0362-1340","1558-1160"],"issn-type":[{"type":"print","value":"0362-1340"},{"type":"electronic","value":"1558-1160"}],"subject":[],"published":{"date-parts":[[2012,9,9]]},"assertion":[{"value":"2012-09-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}