{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:39Z","timestamp":1780994559934,"version":"3.54.1"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2225441"],"award-info":[{"award-number":["2225441"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002808","name":"Carlsbergfondet","doi-asserted-by":"publisher","award":["CF23-0791"],"award-info":[{"award-number":["CF23-0791"]}],"id":[{"id":"10.13039\/501100002808","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101096090"],"award-info":[{"award-number":["101096090"]}],"id":[{"id":"10.13039\/501100000781","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,10,8]]},"abstract":"<jats:p>We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running time of deterministic programs, we introduce a novel notion of probabilistic cost credit. Probabilistic cost credits are a separation logic resource that can be used to pay for the cost of operations in programs, and that can be distributed across all possible branches of sampling instructions according to their weight, thus enabling us to reason about expected cost. The representation of cost credits as separation logic resources gives Tachis a great deal of flexibility and expressivity. In particular, it permits reasoning about amortized expected cost by storing excess credits as potential into data structures to pay for future operations. Tachis further supports a range of cost models, including running time and entropy usage. We showcase the versatility of this approach by applying our techniques to prove upper bounds on the expected cost of a variety of probabilistic algorithms and data structures, including randomized quicksort, hash tables, and meldable heaps. All of our results have been mechanized using Coq, Iris, and the Coquelicot real analysis library.<\/jats:p>","DOI":"10.1145\/3689753","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"1189-1218","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Tachis: Higher-Order Separation Logic with Credits for Expected Costs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0198-7751","authenticated-orcid":false,"given":"Philipp G.","family":"Haselwarter","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4124-5720","authenticated-orcid":false,"given":"Kwing Hei","family":"Li","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3285-5032","authenticated-orcid":false,"given":"Markus","family":"de Medeiros","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6045-5232","authenticated-orcid":false,"given":"Simon Oddershede","family":"Gregersen","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6746-2734","authenticated-orcid":false,"given":"Alejandro","family":"Aguirre","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5692-3347","authenticated-orcid":false,"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473592"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649839"},{"key":"e_1_3_1_7_1","first-page":"13","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (Vancouver, Canada) (LICS \u201919)","author":"Avanzini Martin","year":"2021","unstructured":"Martin Avanzini, Ugo Dal Lago, and Alexis Ghyselen. 2021b. Type-based complexity analysis of probabilistic functional programs. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (Vancouver, Canada) (LICS \u201919). IEEE Press, Article 41, 13 pages."},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428240"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498719"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Thomas Espitau Benjamin Gr\u00e9goire Justin Hsu L\u00e9o Stefanesco and Pierre-Yves Strub. 2015. Relational Reasoning via Probabilistic Coupling. In Logic for Programming Artificial Intelligence and Reasoning - 20th International Conference LPAR-20 2015 Suva Fiji November 24-28 2015 Proceedings. 387\u2013401. https:\/\/doi.org\/10.1007\/978-3-662-48899-7_27 10.1007\/978-3-662-48899-7_27","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2016.107"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571260"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_3_1_17_1","volume-title":"Programming pearls","author":"Bentley Jon Louis","year":"1986","unstructured":"Jon Louis Bentley. 1986. Programming pearls. Addison-Wesley."},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/S11786-014-0181-1"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649824"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1614191"},{"key":"e_1_3_1_22_1","volume-title":"Elements of Information Theory","author":"Cover T.M.","year":"2006","unstructured":"T.M. Cover and J.A. Thomas. 2006. Elements of Information Theory. Wiley."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434313"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/364520.364540"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Hongfei Fu and Krishnendu Chatterjee. 2019. Termination of Nondeterministic Probabilistic Programs. In Verification Model Checking and Abstract Interpretation - 20th International Conference VMCAI 2019 Cascais Portugal January 13-15 2019 Proceedings. 468\u2013490. https:\/\/doi.org\/10.1007\/978-3-030-11245-5_22 10.1007\/978-3-030-11245-5_22","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49477-4_26"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674632"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.556116"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Philipp G. Haselwarter Kwing Hei Li Markus de Medeiros Simon Oddershede Gregersen Alejandro Aguirre Joseph Tassarotti and Lars Birkedal. 2024. Tachis: Higher-Order Separation Logic with Credits for Expected Costs - Coq Artifact. https:\/\/doi.org\/10.5281\/zenodo.12659527 10.5281\/zenodo.12659527","DOI":"10.5281\/zenodo.12659527"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000487"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022670.2951943"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_37_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung David Swasey Filip Sieczkowski Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In ACM-SIGACT Symposium on Principles of Programming Languages.","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009855"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42347"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_4"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591226"},{"key":"e_1_3_1_45_1","volume-title":"Lectures on the Coupling Method","author":"Lindvall T.","year":"2002","unstructured":"T. Lindvall. 2002. Lectures on the Coupling Method. Dover Publications, Incorporated."},{"key":"e_1_3_1_46_1","unstructured":"Janine Lohse and Deepak Garg. 2024. An Iris for Expected Cost Analysis. arXiv:2406.00884 [cs.PL]"},{"key":"e_1_3_1_47_1","unstructured":"J\u00e9r\u00e9mie O. Lumbroso. 2013. Optimal Discrete Uniform Generation from Coin Flips and Applications. CoRR abs\/1304.1916 (2013). arXiv:1304.1916 http:\/\/arxiv.org\/abs\/1304.1916"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/B138392"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_1_50_1","unstructured":"Andrea Mennucci. 2010. Bit recycling for scaling random number generators. CoRR abs\/1012.4290 (2010). arXiv:1012.4290 http:\/\/arxiv.org\/abs\/1012.4290"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/580840"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632892"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","unstructured":"Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In Programming Languages and Systems - 23rd European Symposium on Programming ESOP 2014 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2014 Grenoble France April 5-13 2014 Proceedings. 149\u2013168. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9 10.1007\/978-3-642-54833-8_9","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1002\/bimj.19710130413"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408992"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689753","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689753","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:13:35Z","timestamp":1770196415000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689753"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":58,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689753"],"URL":"https:\/\/doi.org\/10.1145\/3689753","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}