{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,22]],"date-time":"2026-08-22T16:23:00Z","timestamp":1787415780753,"version":"build-2736575974"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,8,22]],"date-time":"2026-08-22T00:00:00Z","timestamp":1787356800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"FWF","award":["P36623"],"award-info":[{"award-number":["P36623"]}]},{"name":"EU Horizon Europe WIDERA","award":["101160022"],"award-info":[{"award-number":["101160022"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,8,22]]},"DOI":"10.1145\/3830439.3831276","type":"proceedings-article","created":{"date-parts":[[2026,8,22]],"date-time":"2026-08-22T15:30:17Z","timestamp":1787412617000},"page":"114-146","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Cost-Aware Probability Monad for Liquid Haskell"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2052-8772","authenticated-orcid":false,"given":"Matthias","family":"Hetzenberger","sequence":"first","affiliation":[{"name":"Vienna University of Technology, Institute of Logic and Computation, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9240-6128","authenticated-orcid":false,"given":"Georg","family":"Moser","sequence":"additional","affiliation":[{"name":"University of Innsbruck, Department of Computer Science, Innsbruck, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Institute of Logic and Computation, Vienna, Austria"},{"name":"TU M\u00fcnchen, TUM School of Computation, Information and Technology (CIT), Munich, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,8,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1137\/S0895480195290017","article-title":"Improved algorithms and analysis for secretary problems and generalizations","volume":"14","author":"Ajtai Miklos","year":"2001","unstructured":"Miklos Ajtai, Nimrod Megiddo, and Orli Waarts. 2001. Improved algorithms and analysis for secretary problems and generalizations. SIAM Journal on Discrete Mathematics 14, 1 (2001), 1\u201327.","journal-title":"SIAM Journal on Discrete Mathematics"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649839"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473592"},{"key":"e_1_3_2_1_5_1","volume-title":"Proc. of the ACM on Programming Languages 4, OOPSLA","author":"Avanzini Martin","year":"2020","unstructured":"Martin Avanzini, Georg Moser, and Michael Schaper. 2020. A Modular Cost Analysis for Probabilistic Programs. Proc. of the ACM on Programming Languages 4, OOPSLA (2020), 172:1\u2013172:30. doi:10.1145\/3428240 10.1145\/3428240"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the ACM on Programming Languages 7, PLDI","author":"Avanzini Martin","year":"2023","unstructured":"Martin Avanzini, Georg Moser, and Michael Schaper. 2023. Automated Expected Value Analysis of Recursive Programs. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 1050\u20131072. doi:10.1145\/3591263 10.1145\/3591263"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Joost-Pieter Katoen and Alexandra Silva (Eds.). 2020. Foundations of Probabilistic Programming. Cambridge University Press. doi:10.1017\/9781108770750 10.1017\/9781108770750","DOI":"10.1017\/9781108770750"},{"key":"e_1_3_2_1_8_1","volume-title":"Proc. ACM Program. Lang. 8, OOPSLA1","author":"Chatterjee Krishnendu","year":"2024","unstructured":"Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. 2024. Quantitative Bounds on Resource Usage of Probabilistic Programs. Proc. ACM Program. Lang. 8, OOPSLA1 (2024), 362\u2013391. doi:10.1145\/3649824 10.1145\/3649824"},{"key":"e_1_3_2_1_9_1","unstructured":"Jacek Cicho\u0144. 2011. Quick Sort - Average Complexity. https:\/\/cs.pwr.edu.pl\/cichon\/Math\/QSortAvg.pdf. Accessed: 2025-07-28."},{"key":"e_1_3_2_1_10_1","volume-title":"Introduction To Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction To Algorithms (3rd ed.). MIT Press. http:\/\/mitpress.mit.edu\/books\/introduction- algorithms","edition":"3"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(84)90009-6","article-title":"Exponential bounds for the running time of a selection algorithm","volume":"29","author":"Devroye Luc","year":"1984","unstructured":"Luc Devroye. 1984. Exponential bounds for the running time of a selection algorithm. J. Comput. System Sci. 29, 1 (1984), 1\u20137.","journal-title":"J. Comput. System Sci."},{"key":"e_1_3_2_1_12_1","unstructured":"Michael Dinitz. 2024. Introduction to Algorithms \u2013 Linear time selection\/median. https:\/\/www.cs.jhu.edu\/~mdinitz\/classes\/IntroAlgorithms\/Fall2024\/schedule\/Lectures\/Lecture4\/lecture4.pdf (archived: https:\/\/web.archive.org\/web\/20260714094747\/https:\/\/www.cs.jhu.edu\/~mdinitz\/classes\/IntroAlgorithms\/Fall2024\/schedule\/Lectures\/Lecture4\/lecture4.pdf ). Accessed: 2026-05-22."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1145\/364520.364540","article-title":"Algorithm 235: random permutation","volume":"7","author":"Durstenfeld Richard","year":"1964","unstructured":"Richard Durstenfeld. 1964. Algorithm 235: random permutation. Commun. ACM 7, 7 (1964), 420.","journal-title":"Commun. ACM"},{"key":"e_1_3_2_1_14_1","volume-title":"Fisher-Yates shuffle. Archive of Formal Proofs (September","author":"Eberl Manuel","year":"2016","unstructured":"Manuel Eberl. 2016. Fisher-Yates shuffle. Archive of Formal Proofs (September 2016). https:\/\/isa- afp.org\/entries\/Fisher_ Yates.html, Formal proof development."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005721"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-"},{"key":"e_1_3_2_1_18_1","volume-title":"Proc. 25th SOFSEM (LNCS","volume":"349","author":"Gambin Anna","year":"1998","unstructured":"Anna Gambin and Adam Malinowski. 1998. Randomized Meldable Priority Queues. In Proc. 25th SOFSEM (LNCS, Vol. 1521), Branislav Rovan (Ed.). 344\u2013349. doi:10.1007\/3- 540- 49477- 4_26 10.1007\/3-540-49477-4_26"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"e_1_3_2_1_20_1","volume-title":"Proc. ACM Program. Lang. 8, OOPSLA2","author":"Haselwarter Philipp G.","year":"2024","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. Proc. ACM Program. Lang. 8, OOPSLA2 (2024), 1189\u20131218. doi:10.1145\/3689753 10.1145\/3689753"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Matthias Hetzenberger Georg Moser and Florian Zuleger. 2026. A Cost-Aware Probability Monad for Liquid Haskell: Haskell Artifact. doi:10.5281\/zenodo.21397698 10.5281\/zenodo.21397698","DOI":"10.5281\/zenodo.21397698"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/366622.366647"},{"key":"e_1_3_2_1_23_1","volume-title":"Proc. 44th POPL, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 359\u2013373","author":"Hoffmann Jan","year":"2017","unstructured":"Jan Hoffmann, Ankush Das, and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In Proc. 44th POPL, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 359\u2013373. doi:10.1145\/3009837.3009842 10.1145\/3009837.3009842"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000232"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen and Christoph Matheja. 2020. Expected Runtime Analysis by Program Verification. In Foundations of Probabilistic Programming. 185\u2013220. doi:10.1017\/9781108770750.007 10.1017\/9781108770750.007","DOI":"10.1017\/9781108770750.007"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050057"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","article-title":"Semantics of Probabilistic Programs","volume":"22","author":"Kozen Dexter","year":"1981","unstructured":"Dexter Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22, 3 (1981), 328\u2013350.","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-"},{"key":"e_1_3_2_1_30_1","volume-title":"Proc. 33rd CAV (LNCS","volume":"122","author":"Leutgeb Lorenz","year":"2021","unstructured":"Lorenz Leutgeb, Georg Moser, and Florian Zuleger. 2021. ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. In Proc. 33rd CAV (LNCS, Vol. 12760). 99\u2013122. doi:10.1007\/978- 3- 030- 81688- 9_5 10.1007\/978-3-030-81688-9_5"},{"key":"e_1_3_2_1_31_1","volume-title":"Proc. 34th CAV (LNCS","volume":"91","author":"Leutgeb Lorenz","year":"2022","unstructured":"Lorenz Leutgeb, Georg Moser, and Florian Zuleger. 2022. Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In Proc. 34th CAV (LNCS, Vol. 13372). 70\u201391. doi:10.1007\/978- 3- 031- 13188- 2_4 10.1007\/978-3-031-13188-2_4"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/274787.274812"},{"key":"e_1_3_2_1_33_1","volume-title":"Automated reasoning and randomization in separation logic. Ph. D. Dissertation","author":"Matheja Christoph","unstructured":"Christoph Matheja. 2020. Automated reasoning and randomization in separation logic. Ph. D. Dissertation. RWTH Aachen University, Germany. https:\/\/publications.rwth- aachen.de\/record\/780877"},{"key":"e_1_3_2_1_34_1","volume-title":"Proc. 30th ESOP (LNCS","volume":"518","author":"Moosbrugger Marcel","year":"2021","unstructured":"Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, and Laura Kov\u00e1cs. 2021. Automated Termination Analysis of Polynomial Probabilistic Programs. In Proc. 30th ESOP (LNCS, Vol. 12648). 491\u2013518. doi:10.1007\/978- 3- 030- 72019- 3_18 10.1007\/978-3-030-72019-3_18"},{"key":"e_1_3_2_1_35_1","volume-title":"Proc. of 39th PLDI. ACM, 496\u2013512","author":"Ngo Van Chan","year":"2018","unstructured":"Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2018. Bounded Expectations: Resource Analysis for Probabilistic Programs. In Proc. of 39th PLDI. ACM, 496\u2013512. doi:10.1145\/3296979.3192394 10.1145\/3296979.3192394"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/s10817-018-9459-3","article-title":"Amortized Complexity Verified","volume":"62","author":"Nipkow Tobias","year":"2019","unstructured":"Tobias Nipkow and Hauke Brinkop. 2019. Amortized Complexity Verified. JAR 62, 3 (2019), 367\u2013391.","journal-title":"JAR"},{"key":"e_1_3_2_1_37_1","volume-title":"Purely functional data structures","author":"Okasaki C.","unstructured":"C. Okasaki. 1999. Purely functional data structures. Cambridge University Press."},{"key":"e_1_3_2_1_38_1","volume-title":"Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Ramsey Norman","year":"2002","unstructured":"Norman Ramsey and Avi Pfeffer. 2002. Stochastic lambda calculus and monads of probability distributions. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, Oregon) (POPL \u201902). Association for Computing Machinery, New York, NY, USA, 154\u2013165. doi:10.1145\/503272.503288 10.1145\/503272.503288"},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell. 165\u2013176","author":"\u015acibior Adam","year":"2015","unstructured":"Adam \u015acibior, Zoubin Ghahramani, and Andrew D Gordon. 2015. Practical probabilistic programming with monads. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell. 165\u2013176."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1145\/3828.3835","article-title":"Self-adjusting binary search trees","volume":"32","author":"Sleator Daniel Dominic","year":"1985","unstructured":"Daniel Dominic Sleator and Robert Endre Tarjan. 1985. Self-adjusting binary search trees. Journal of the ACM (JACM) 32, 3 (1985), 652\u2013686.","journal-title":"Journal of the ACM (JACM)"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1137\/0606031","article-title":"Amortized computational complexity","volume":"6","author":"Tarjan Robert Endre","year":"1985","unstructured":"Robert Endre Tarjan. 1985. Amortized computational complexity. SIAM Journal on Algebraic Discrete Methods 6, 2 (1985), 306\u2013318.","journal-title":"SIAM Journal on Algebraic Discrete Methods"},{"key":"e_1_3_2_1_42_1","volume-title":"Proc. 9th ITP (LNCS), Jeremy Avigad and Assia Mahboubi (Eds.). 560\u2013578","author":"Tassarotti Joseph","year":"2018","unstructured":"Joseph Tassarotti and Robert Harper. 2018. Verified Tail Bounds for Randomized Programs. In Proc. 9th ITP (LNCS), Jeremy Avigad and Assia Mahboubi (Eds.). 560\u2013578. doi:10.1007\/978- 3- 319- 94821- 8_33 10.1007\/978-3-319-94821-8_33"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_2_1_44_1","volume-title":"Proceedings of the 17th ACM SIGPLAN International Haskell Symposium (Haskell \u201824)","author":"van Br\u00fcgge Jan","year":"2024","unstructured":"Jan van Br\u00fcgge. 2024. Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl). In Proceedings of the 17th ACM SIGPLAN International Haskell Symposium (Haskell \u201824). ACM, 97\u2013108. doi:10.1145\/3677999.3678282 10.1145\/3677999.3678282"},{"key":"e_1_3_2_1_45_1","volume-title":"Types for Proofs and Programs, Stefano Berardi, Ferruccio Damiani, and Ugo de\u2019Liguoro (Eds.)","author":"van der Weegen Eelis","unstructured":"Eelis van der Weegen and James McKinna. 2009. A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. In Types for Proofs and Programs, Stefano Berardi, Ferruccio Damiani, and Ugo de\u2019Liguoro (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 256\u2013271."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547643"},{"key":"e_1_3_2_1_47_1","volume-title":"Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell (St","author":"Vazou Niki","year":"2018","unstructured":"Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, and Graham Hutton. 2018. Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell (St. Louis, MO, USA) (Haskell 2018). Association for Computing Machinery, New York, NY, USA, 132\u2013144. doi:10.1145\/3242744.3242756 10.1145\/3242744.3242756"},{"key":"e_1_3_2_1_48_1","volume-title":"Proceedings of the 19th ACM SIGPLAN international conference on Functional programming","author":"Vazou Niki","year":"2014","unstructured":"Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 269\u2013282."},{"key":"e_1_3_2_1_49_1","first-page":"10","volume-title":"Proc. ACM Program. Lang. 2, POPL, Article 53 (Dec.","author":"Vazou Niki","year":"2017","unstructured":"Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. 2017. Refinement reflection: complete verification with SMT. Proc. ACM Program. Lang. 2, POPL, Article 53 (Dec. 2017), 31 pages. doi:10.1145\/3158141 10.1145\/3158141"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408992"},{"key":"e_1_3_2_1_51_1","volume-title":"Proc. of 40th PLDI. ACM, 204\u2013220","author":"Wang P.","unstructured":"P. Wang, H. Fu, A. K. Goharshady, K. Chatterjee, X. Qin, and W. Shi. 2019. Cost Analysis of Nondeterministic Probabilistic Programs. In Proc. of 40th PLDI. ACM, 204\u2013220."},{"key":"e_1_3_2_1_52_1","volume-title":"Proc. ACM Program. Lang. 9, POPL","author":"Zaiser Fabian","year":"2025","unstructured":"Fabian Zaiser, Andrzej S. Murawski, and C.-H. Luke Ong. 2025. Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops. Proc. ACM Program. Lang. 9, POPL (2025), 1104\u20131135. doi:10.1145\/3704874 10.1145\/3704874"}],"event":{"name":"Haskell '26: 19th ACM SIGPLAN International Haskell Symposium","location":"Indianapolis IN USA","acronym":"Haskell '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 19th ACM SIGPLAN International Haskell Symposium"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3830439.3831276","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,22]],"date-time":"2026-08-22T15:30:27Z","timestamp":1787412627000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3830439.3831276"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8,22]]},"references-count":52,"alternative-id":["10.1145\/3830439.3831276","10.1145\/3830439"],"URL":"https:\/\/doi.org\/10.1145\/3830439.3831276","relation":{},"subject":[],"published":{"date-parts":[[2026,8,22]]},"assertion":[{"value":"2026-08-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}