{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T16:10:03Z","timestamp":1787069403399,"version":"build-2736575974"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n                    A thunk is a mutable data structure that offers a simple memoization service: it stores either a suspended computation or the result of this computation.\n                    <jats:xref ref-type=\"bibr\">Okasaki [1999]<\/jats:xref>\n                    presents many data structures that exploit thunks to achieve good amortized time complexity. He analyzes their complexity by associating a debit with every thunk. A debit can be paid off in several increments; a thunk whose debit has been fully paid off can be forced. Quite strikingly, a debit is associated also with future thunks, which do not yet exist in memory. Some of the debit of a faraway future thunk can be transferred to a nearer future thunk. We present a complete machine-checked reconstruction of Okasaki\u2019s reasoning rules in Iris\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msup>\n                          <mml:mrow\/>\n                          <mml:mi>$<\/mml:mi>\n                        <\/mml:msup>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    , a rich separation logic with time credits. We demonstrate the applicability of the rules by verifying a few operations on streams as well as several of Okasaki\u2019s data structures, namely the physicist\u2019s queue, implicit queues, and the banker\u2019s queue.\n                  <\/jats:p>","DOI":"10.1145\/3632892","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"1482-1508","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Thunks and Debits in Separation Logic with Time Credits"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4069-1235","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Pottier","sequence":"first","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3072-4045","authenticated-orcid":false,"given":"Arma\u00ebl","family":"Gu\u00e9neau","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - Laboratoire M\u00e9thodes Formelles, Gif-sur-Yvette, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9781-7097","authenticated-orcid":false,"given":"Jacques-Henri","family":"Jourdan","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay - CNRS - ENS Paris-Saclay - Laboratoire M\u00e9thodes Formelles, Gif-sur-Yvette, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1816-7605","authenticated-orcid":false,"given":"Glen","family":"M\u00e9vel","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - Laboratoire M\u00e9thodes Formelles, Gif-sur-Yvette, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"issue":"2","key":"e_1_3_1_2_2","article-title":"Amortised Resource Analysis with Separation Logic","volume":"7","author":"Atkey Robert","year":"2011","unstructured":"Robert Atkey. 2011. Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science 7, 2:17 (2011). http:\/\/bentnib.org\/amortised-sep-logic-journal.pdf","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_1_3_2","article-title":"Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits","author":"Chargu\u00e9raud Arthur","year":"2017","unstructured":"Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2017. Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. Journal of Automated Reasoning (Sept. 2017). http:\/\/cambium.inria.fr\/~fpottier\/publis\/chargueraud-pottier-uf-sltc.pdf","journal-title":"Journal of Automated Reasoning (Sept. 2017)"},{"key":"e_1_3_1_4_2","article-title":"Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures","author":"Danielsson Nils Anders","year":"2008","unstructured":"Nils Anders Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Principles of Programming Languages (POPL). http:\/\/www.cse.chalmers.se\/~nad\/publications\/danielsson-popl2008. pdf","journal-title":"Principles of Programming Languages (POPL)"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","unstructured":"James R. Driscoll Neil Sarnak Daniel Dominic Sleator and Robert Endre Tarjan. 1989. Making Data Structures Persistent. J. Comput. System Sci. 38 1 (1989) 86\u2013124. https:\/\/doi.org\/10.1016\/0022-0000(89)90034-2 10.1016\/0022-0000(89)90034-2","DOI":"10.1016\/0022-0000(89)90034-2"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Jennifer Hackett and Graham Hutton. 2019. Call-by-need is clairvoyant call-by-value. Proceedings of the ACM on Programming Languages 3 ICFP (2019) 114:1\u2013114:23. https:\/\/doi.org\/10.1145\/3341718 10.1145\/3341718","DOI":"10.1145\/3341718"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Martin A. T. Handley Niki Vazou and Graham Hutton. 2020. Liquidate your assets: reasoning about resource usage in Liquid Haskell. Proceedings of the ACM on Programming Languages 4 POPL (2020) 24:1\u201324:27. https:\/\/doi.org\/10.1145\/3371092 10.1145\/3371092","DOI":"10.1145\/3371092"},{"key":"e_1_3_1_8_2","first-page":"292","volume-title":"European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 12648)","author":"Haslbeck Maximilian P. L.","year":"2021","unstructured":"Maximilian P. L. Haslbeck and Peter Lammich. 2021. For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 12648). Springer, 292\u2013319. https:\/\/www21.in.tum.de\/~haslbema\/documents\/Haslbeck_Lammich_LLVM_with_Time.pdf"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_9"},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","unstructured":"Jan Hoffmann Michael Marmar and Zhong Shao. 2013. Quantitative Reasoning for Proving Lock-Freedom. In Logic in Computer Science (LICS). 124\u2013133. http:\/\/www.cs.cmu.edu\/~janh\/papers\/lockfree2013.pdf","DOI":"10.1109\/LICS.2013.18"},{"key":"e_1_3_1_11_2","doi-asserted-by":"crossref","unstructured":"John Hughes. 1989. Why Functional Programming Matters. Computer Journal 32 2 (1989) 98\u2013107. http:\/\/www.cse.chalmers.se\/~rjmh\/Papers\/whyfp.pdf","DOI":"10.1093\/comjnl\/32.2.98"},{"key":"e_1_3_1_12_2","doi-asserted-by":"crossref","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018) e20. https:\/\/people.mpi-sws.org\/~dreyer\/papers\/iris-ground-up\/paper.pdf","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Yao Li Li-yao Xia and Stephanie Weirich. 2021. Reasoning about the garden of forking paths. Proceedings of the ACM on Programming Languages 5 ICFP (2021) 1\u201328. https:\/\/doi.org\/10.1145\/3473585 10.1145\/3473585","DOI":"10.1145\/3473585"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009874"},{"key":"e_1_3_1_15_2","doi-asserted-by":"crossref","unstructured":"Simon Marlow Simon L. Peyton Jones and Satnam Singh. 2009. Runtime support for multicore Haskell. In International Conference on Functional Programming (ICFP). 65\u201378. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2009\/09\/multicore-ghc.pdf","DOI":"10.1145\/1596550.1596563"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_10"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_1_18_2","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow and Hauke Brinkop. 2019. Amortized Complexity Verified. Journal of Automated Reasoning 62 3 (2019) 367\u2013391. https:\/\/www21.in.tum.de\/~nipkow\/pubs\/jar18.pdf","DOI":"10.1007\/s10817-018-9459-3"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104"},{"key":"e_1_3_1_20_2","doi-asserted-by":"crossref","unstructured":"Alexandre Pilkiewicz and Fran\u00e7ois Pottier. 2011. The essence of monotonic state. In Types in Language Design and Implementation (TLDI). http:\/\/cambium.inria.fr\/~fpottier\/publis\/pilkiewicz-pottier-monotonicity.pdf","DOI":"10.1145\/1929553.1929565"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Pottier Arma\u00ebl Gu\u00e9neau Jacques-Henri Jourdan and Glen M\u00e9vel. 2023. Thunks and Debits in Separation Logic with Time Credits: Coq Formalization. https:\/\/gitlab.inria.fr\/cambium\/iris-time-proofs.","DOI":"10.1145\/3632892"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Robert Endre Tarjan. 1985. Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods 6 2 (1985) 306\u2013318. http:\/\/dx.doi.org\/10.1137\/0606031 10.1137\/0606031","DOI":"10.1137\/0606031"},{"key":"e_1_3_1_23_2","doi-asserted-by":"crossref","unstructured":"Bohua Zhan and Maximilian P. L. Haslbeck. 2018. Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. In International Joint Conference on Automated Reasoning. http:\/\/arxiv.org\/abs\/1802.01336","DOI":"10.1007\/978-3-319-94205-6_35"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632892","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632892","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:05:00Z","timestamp":1751645100000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632892"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":22,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632892"],"URL":"https:\/\/doi.org\/10.1145\/3632892","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}