{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T03:48:45Z","timestamp":1787456925625,"version":"build-2736575974"},"reference-count":76,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["DIAPASoN GA 818616"],"award-info":[{"award-number":["DIAPASoN GA 818616"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-19-CE48-0014"],"award-info":[{"award-number":["ANR-19-CE48-0014"]}],"id":[{"id":"10.13039\/501100001665","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":[[2021,8,22]]},"abstract":"<jats:p>\n            We define a continuation-passing style (CPS) translation for a typed \u03bb-calculus with probabilistic choice, unbounded recursion, and a tick operator \u2014 for modeling cost. The target language is a (non-probabilistic) \u03bb-calculus, enriched with a type of extended positive reals and a fixpoint operator. We then show that applying the CPS transform of an expression\n            <jats:italic>M<\/jats:italic>\n            to the continuation \u03bb\n            <jats:italic>v<\/jats:italic>\n            . 0 yields the expected cost of\n            <jats:italic>M<\/jats:italic>\n            . We also introduce a formal system for higher-order logic, called EHOL, prove it sound, and show it can derive tight upper bounds on the expected cost of classic examples, including Coupon Collector and Random Walk. Moreover, we relate our translation to Kaminski et al.\u2019s ert-calculus, showing that the latter can be recovered by applying our CPS translation to (a generalization of) the classic embedding of imperative programs into \u03bb-calculus. Finally, we prove that the CPS transform of an expression can also be used to compute pre-expectations and to reason about almost sure termination.\n          <\/jats:p>","DOI":"10.1145\/3473592","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["On continuation-passing transformations and expected cost analysis"],"prefix":"10.1145","volume":"5","author":[{"given":"Martin","family":"Avanzini","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785725"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_2_2_8_1","first-page":"102338","article-title":"On Probabilistic Term Rewriting","volume":"185","author":"Avanzini M.","year":"2019","journal-title":"SCP"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428240"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.06.005"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003833"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11526841_9"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_6"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408979"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434313"},{"key":"e_1_2_2_24_1","volume-title":"Linear Dependent Types and Relative Completeness. Log. Methods Comput. Sci., 8, 4","author":"Lago Ugo Dal","year":"2011"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293605"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2012012"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001535"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00733-8"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1515\/9781400882618-010"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535865"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3164540"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.39"},{"key":"e_1_2_2_35_1","volume-title":"Representing Monads. In Conference Record of POPL\u201994: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Filinski Andrzej","year":"1994"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90070-9"},{"key":"e_1_2_2_38_1","volume-title":"Church: A Language for Generative Models. In UAI. 220\u2013229.","author":"Goodman N. D.","year":"2008"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785809"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/800119.803889"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80216-6"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005153"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_2_47_1","doi-asserted-by":"crossref","unstructured":"B. L. Kaminski J.-P. Katoen C. Matheja and F. Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. JACM 65 5 (2018) 30:1\u201330:68.  B. L. Kaminski J.-P. Katoen C. Matheja and F. Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. JACM 65 5 (2018) 30:1\u201330:68.","DOI":"10.1145\/3208102"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_7"},{"key":"e_1_2_2_55_1","volume-title":"Randomized Algorithms","author":"Motwani Rajeev"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90029-3"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(63)90290-0"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503288"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99381"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08921-7_92"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1969-0249221-4"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158148"},{"key":"e_1_2_2_68_1","unstructured":"R. Sedgewick and P. Flajolet. 1996. An Introduction to the Analysis of Algorithms. Addison-Wesley-Longman. isbn:978-0-201-40009-0  R. Sedgewick and P. Flajolet. 1996. An Introduction to the Analysis of Algorithms. Addison-Wesley-Longman. isbn:978-0-201-40009-0"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_28"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_28"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064899.3064910"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192408"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408992"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/361002.361016"},{"key":"e_1_2_2_76_1","doi-asserted-by":"crossref","volume-title":"The Formal Semantics of Programming Languages","author":"Winskel G.","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473592","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473592","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473592"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":76,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473592"],"URL":"https:\/\/doi.org\/10.1145\/3473592","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}