{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:25:16Z","timestamp":1787592316817,"version":"build-2736575974"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["BLAST"],"award-info":[{"award-number":["BLAST"]}],"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":[[2025,4,9]]},"abstract":"<jats:p>Reasoning about the cost of executing programs is one of the fundamental questions in computer science. In the context of programming with probabilities, however, the notion of cost stops being deterministic, since it depends on the probabilistic samples made throughout the execution of the program. This interaction is further complicated by the non-trivial interaction between cost, recursion and evaluation strategy.<\/jats:p>\n                  <jats:p>\n                    In this work we introduce\n                    <jats:bold>cert<\/jats:bold>\n                    : a Call-By-Push-Value (CBPV) metalanguage for reasoning about probabilistic cost. We equip\n                    <jats:bold>cert<\/jats:bold>\n                    with an operational cost semantics and define two denotational semantics \u2014 a cost semantics and an expected-cost semantics. We prove operational soundness and adequacy for the denotational cost semantics and a cost adequacy theorem for the expected-cost semantics.\n                  <\/jats:p>\n                  <jats:p>\n                    We formally relate both denotational semantics by stating and proving a novel\n                    <jats:italic toggle=\"yes\">effect simulation<\/jats:italic>\n                    property for CBPV. We also prove a canonicity property of the expected-cost semantics as the minimal semantics for expected cost and probability by building on recent advances on monadic probabilistic semantics.\n                  <\/jats:p>\n                  <jats:p>\n                    Finally, we illustrate the expressivity of\n                    <jats:bold>cert<\/jats:bold>\n                    and the expected-cost semantics by presenting case-studies ranging from randomized algorithms to stochastic processes and show how our semantics capture their intended expected cost.\n                  <\/jats:p>","DOI":"10.1145\/3720424","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"280-306","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Denotational Foundations for Expected Cost Analysis"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8338-8973","authenticated-orcid":false,"given":"Pedro H.","family":"Azevedo de Amorim","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","unstructured":"Alejandro Aguirre Shin-ya Katsumata and Satoshi Kura. 2022. Weakest preconditions in fibrations. Mathematical Structures in Computer Science (2022). doi:10.1017\/S0960129522000330","DOI":"10.1017\/S0960129522000330"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","unstructured":"Martin Avanzini Gilles Barthe and Ugo Dal Lago. 2021. On continuation-passing transformations and expected cost analysis. In International Conference on Functional Programming (ICFP). doi:10.1145\/3473592","DOI":"10.1145\/3473592"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Martin Avanzini Ugo Dal Lago and Alexis Ghyselen. 2019. Type-based complexity analysis of probabilistic functional programs. In Logic in Computer Science (LICS). doi:doi:10.1109\/LICS.2019.8785725","DOI":"10.1109\/LICS.2019.8785725"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","unstructured":"Martin Avanzini Georg Moser and Michael Schaper. 2020. A modular cost analysis for probabilistic programs. In Object-oriented Programming Systems Languages and Applications (OOPSLA). doi:10.1145\/3428240","DOI":"10.1145\/3428240"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Kevin Batz Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Lena Verscht. 2023. A calculus for amortized expected runtimes. doi:10.1145\/3571260","DOI":"10.1145\/3571260"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525858"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","unstructured":"Titouan Carette Louis Lemonnier and Vladimir Zamdzhiev. 2023. Central submonads and notions of computation: Soundness completeness and internal languages. In Logic in Computer Science (LICS). doi:10.1109\/LICS56636.2023.10175687","DOI":"10.1109\/LICS56636.2023.10175687"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Hongfei Fu Petr Novotn\u00fd and Rouzbeh Hasheminezhad. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In Principles of Programming Languages (POPL). doi:10.1145\/3174800","DOI":"10.1145\/3174800"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Ezgi \u00c7i\u00e7ek Gilles Barthe Marco Gaboardi Deepak Garg and Jan Hoffmann. 2017. Relational cost analysis. In Principles of Programming Languages (POPL). doi:10.1145\/3009837.3009858","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","unstructured":"Joseph W Cutler Daniel R Licata and Norman Danner. 2020. Denotational recurrence extraction for amortized analysis. doi:10.1145\/3408979","DOI":"10.1145\/3408979"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","unstructured":"Norman Danner Daniel R Licata and Ramyaa Ramyaa. 2015. Denotational cost semantics for functional languages with inductive types. In International Conference on Functional Programming (ICFP). doi:10.1145\/2784731.2784749","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Norman Danner Jennifer Paykin and James S Royer. 2013. A static cost analysis for a higher-order language. In 7th workshop on Programming languages meets program verification. doi:10.1145\/2428116.2428123","DOI":"10.1145\/2428116.2428123"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158147"},{"key":"e_1_3_1_15_2","volume-title":"Controlling Effects","author":"Filinski Andrzej","year":"1996","unstructured":"Andrzej Filinski. 1996. Controlling Effects. Ph. D. Dissertation. School of Computer Science, Carnegie Mellon University."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Mordecai Golin and Robert Sedgewick. 1988. Analysis of a simple yet efficient convex hull algorithm. In Proceedings of the fourth annual symposium on Computational geometry. doi:10.1145\/73393.73409","DOI":"10.1145\/73393.73409"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","unstructured":"Harrison Grodin Yue Niu Jonathan Sterling and Robert Harper. 2023. Decalf: A Directed Effectful Cost-Aware Logical Framework. In Principles of Programming Languages (POPL). doi:10.1145\/3632852","DOI":"10.1145\/3632852"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"J. Grosen D. M. Kahn and J. Hoffmann. 2023. Automatic Amortized Resource Analysis with Regular Recursive Types. In Logic in Computer Science (LICS). doi:10.1109\/LICS56636.2023.10175720","DOI":"10.1109\/LICS56636.2023.10175720"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Chris Heunen Ohad Kammar Sam Staton and Hongseok Yang. 2017. A Convenient Category for Higher-Order Probability Theory. In Logic in Computer Science (LICS). doi:10.1109\/LICS.2017.8005137","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In Symposium on Principles of Programming Languages (POPL). doi:10.1145\/3009837.3009842","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Jan Hoffmann and Zhong Shao. 2015. Automatic static cost analysis for parallel programs. In European Symposium on Programming (ESOP). doi:10.1007\/978-3-662-46669-8_6","DOI":"10.1007\/978-3-662-46669-8_6"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"David M Kahn and Jan Hoffmann. 2020. Exponential automatic amortized resource analysis. In Foundations of Software Science and Computation Structures (FoSSaCS). doi:10.1007\/978-3-030-45231-5_19","DOI":"10.1007\/978-3-030-45231-5_19"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2016. Weakest precondition reasoning for expected run\u2013times of probabilistic programs. In European Symposium on Programming (ESOP). doi:10.1007\/978-3-662-49498-1_15","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","unstructured":"Ohad Kammar and Dylan McDermott. 2018. Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics. Electronic notes in theoretical computer science (2018). doi:10.1016\/j.entcs.2018.11.012","DOI":"10.1016\/j.entcs.2018.11.012"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Shin-ya Katsumata. 2013. Relating computational effects by \u22a4\u22a4-lifting. Information and Computation (2013). doi:10.1007\/978-3-642-22012-8_13","DOI":"10.1007\/978-3-642-22012-8_13"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","unstructured":"Shin-ya Katsumata Tetsuya Sato and Tarmo Uustalu. 2018. Codensity lifting of monads and its dual. Logical Methods in Computer Science (2018). doi:10.23638\/LMCS-14(4:6)2018","DOI":"10.23638\/LMCS-14(4:6)2018"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","unstructured":"GA Kavvos Edward Morehouse Daniel R Licata and Norman Danner. 2019. Recurrence extraction for functional programs through call-by-push-value. In Principles of Programming Languages (POPL). doi:10.1145\/3371083","DOI":"10.1145\/3371083"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 1983. A Probabilistic PDL. In Symposium on Theory of Computing (STOC). doi:10.1016\/0022-0000(85)90012-1","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","unstructured":"Satoshi Kura Natsuki Urabe and Ichiro Hasuo. 2019. Tail probabilities for randomized program runtimes via martingales for higher moments. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). doi:10.1007\/978-3-030-17465-1_8","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","unstructured":"Lorenz Leutgeb Georg Moser and Florian Zuleger. 2022. Automated expected amortised cost analysis of probabilistic data structures. In Computer Aided Verification (CAV). doi:10.1007\/978-3-031-13188-2_4","DOI":"10.1007\/978-3-031-13188-2_4"},{"key":"e_1_3_1_31_2","unstructured":"Paul Blain Levy. 2001. Call-by-push-value. Ph. D. Dissertation."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","unstructured":"Benjamin Lichtman and Jan Hoffmann. 2017. Arrays and references in resource aware ML. In Formal Structures for Computation and Deduction (FSCD 2017). doi:10.4230\/LIPIcs.FSCD.2017.26","DOI":"10.4230\/LIPIcs.FSCD.2017.26"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","unstructured":"Eugenio Moggi. 1989. Computational lambda-calculus and monads. In Logic in Computer Science (LICS). doi:10.1109\/LICS.1989.39155","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","unstructured":"Van Chan Ngo Quentin Carbonneaux and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. In Programming Language Design and Implementation (PLDI). doi:10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","unstructured":"Yue Niu Jonathan Sterling Harrison Grodin and Robert Harper. 2022. A cost-aware logical framework. In Principles of Programming Languages (POPL). doi:10.1145\/3498670","DOI":"10.1145\/3498670"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","unstructured":"Franco P Preparata and Michael I Shamos. 2012. Computational geometry: an introduction. Springer Science & Business Media. doi:10.1007\/978-1-4612-1098-6","DOI":"10.1007\/978-1-4612-1098-6"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689725"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","unstructured":"Vineet Rajani Marco Gaboardi Deepak Garg and Jan Hoffmann. 2021. A unifying type-theory for higher-order (amortized) cost analysis. In Symposium on Principles of Programming Languages (POPL). doi:10.1145\/3434308","DOI":"10.1145\/3434308"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","unstructured":"Yican Sun Hongfei Fu Krishnendu Chatterjee and Amir Kafshdar Goharshady. 2023. Automated Tail Bound Analysis for Probabilistic Recurrence Relations. In Computer Aided Verification (CAV). doi:10.1007\/978-3-031-37709-9_2","DOI":"10.1007\/978-3-031-37709-9_2"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","unstructured":"Matthijs V\u00e1k\u00e1r Ohad Kammar and Sam Staton. 2019. A domain theory for statistical probabilistic programming. In Principles of Programming Languages (POPL). doi:10.1145\/3290349","DOI":"10.1145\/3290349"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Di Wang David M Kahn and Jan Hoffmann. 2020. Raising expectations: automating expected cost analysis with types. International Conference on Functional Programming (ICFP). doi:10.1145\/3408992","DOI":"10.1145\/3408992"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","unstructured":"Peng Wang Di Wang and Adam Chlipala. 2017. TiML: a functional language for practical complexity analysis with invariants. In Object-oriented Programming Systems Languages and Applications (OOPSLA). doi:10.1145\/3133903","DOI":"10.1145\/3133903"},{"key":"e_1_3_1_44_2","unstructured":"Gavin C. Wraith. 1970. Algebraic Theories. Lecture notes Aarhus University."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720424","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720424","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:32:03Z","timestamp":1787589123000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720424"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":43,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720424"],"URL":"https:\/\/doi.org\/10.1145\/3720424","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}