{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:41Z","timestamp":1780994561866,"version":"3.54.1"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"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,8,15]]},"abstract":"<jats:p>\n                    Almost-sure termination is an important correctness property for probabilistic programs, and a number of program logics have been developed for establishing it. However, these logics have mostly been developed for first-order programs written in languages with specific syntactic patterns for looping. In this paper, we consider almost-sure termination for higher-order probabilistic programs with general references. This combination of features allows for recursion and looping to be encoded through a variety of patterns. Therefore, rather than developing proof rules for reasoning about particular recursion patterns, we instead propose an approach based on proving\n                    <jats:italic toggle=\"yes\">refinement<\/jats:italic>\n                    between a higher-order program and a simpler probabilistic model, in such a way that the refinement preserves termination behavior. By proving a refinement, almost-sure termination behavior of the program can then be established by analyzing the simpler model.\n                  <\/jats:p>\n                  <jats:p>\n                    We present this approach in the form of\n                    <jats:monospace>Caliper<\/jats:monospace>\n                    , a higher-order separation logic for proving terminationpreserving refinements.\n                    <jats:monospace>Caliper<\/jats:monospace>\n                    uses probabilistic couplings to carry out relational reasoning between a program and a model. To handle the range of recursion patterns found in higher-order programs,\n                    <jats:monospace>Caliper<\/jats:monospace>\n                    uses guarded recursion, in particular the principle of L\u00f6b induction. A technical novelty is that\n                    <jats:monospace>Caliper<\/jats:monospace>\n                    does not require the use of transfinite step indexing or other technical restrictions found in prior work on guarded recursion for termination-preservation refinement. We demonstrate the flexibility of this approach by proving almost-sure termination of several examples, including first-order loop constructs, a random list generator, treaps, and a sampler for Galton-Watson trees that uses higher-order store. All the results have been mechanized in the Coq proof assistant.\n                  <\/jats:p>","DOI":"10.1145\/3674632","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"203-233","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Almost-Sure Termination by Guarded Refinement"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6045-5232","authenticated-orcid":false,"given":"Simon Oddershede","family":"Gregersen","sequence":"first","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-0003-0198-7751","authenticated-orcid":false,"given":"Philipp G.","family":"Haselwarter","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,8,15]]},"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.1007\/978-3-319-89884-1_8"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571195"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel Paul-Andr\u00e9 Melli\u00e8s Christopher D. Richards and J\u00e9r\u00f4me Vouillon. 2007. A very modal model of a modern major general type system. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2007 Nice France January 17-19 2007. 109\u2013122. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_6"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-65371-1"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473592"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_1_11_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2023. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https:\/\/iris-project.org\/tutorial-pdfs\/iris-lecture-notes.pdf"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Ales Bizjak and Lars Birkedal. 2015. Step-Indexed Logical Relations for Probability. In Foundations of Software Science and Computation Structures - 18th International Conference FoSSaCS 2015 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2015 London UK April 11-18 2015. Proceedings. 279\u2013294. https:\/\/doi.org\/10.1007\/978-3-662-46678-0_18 10.1007\/978-3-662-46678-0_18","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0181-1"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-012-0166-0"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verification - 25th International Conference CAV 2013 Saint Petersburg Russia July 13-19 2013. Proceedings. 511\u2013526. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34 10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-017-9431-7"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-6956-8"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Coq Development Team. 2023. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.8161141 10.5281\/zenodo.8161141","DOI":"10.5281\/zenodo.8161141"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1137\/090766632"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-020-09545-0"},{"key":"e_1_3_1_24_1","unstructured":"Jeff Erickson. 2017. Treaps and Skip Lists. https:\/\/jeffe.cs.illinois.edu\/teaching\/algorithms\/notes\/03-treaps.pdf Lecture notes."},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462153.1462154"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586051"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00003"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_1_31_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_32_1","doi-asserted-by":"publisher","unstructured":"Simon Oddershede Gregersen Alejandro Aguirre Philipp G. Haselwarter Joseph Tassarotti and Lars Birkedal. 2024a. Almost-Sure Termination by Guarded Refinement - Coq Artifact. https:\/\/doi.org\/10.5281\/zenodo.11481248 10.5281\/zenodo.11481248","DOI":"10.5281\/zenodo.11481248"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357214"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_16"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","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 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2015 Mumbai India January 15-17 2015. 637\u2013650. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00236-018-0321-1"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In Programming Languages and Systems - 25th European Symposium on Programming ESOP 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2016 Eindhoven The Netherlands April 2-8 2016 Proceedings. 364\u2013389. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15 10.1007\/978-3-662-49498-1_15","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi Ugo Dal Lago and Charles Grellois. 2019. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. In 34th Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2019 Vancouver BC Canada June 24-27 2019. 1\u201314. https:\/\/doi.org\/10.1109\/LICS.2019.8785679 10.1109\/LICS.2019.8785679","DOI":"10.1109\/LICS.2019.8785679"},{"issue":"4","key":"e_1_3_1_42_1","article-title":"On the Termination Problem for Probabilistic Higher-Order Recursive Programs","volume":"16","author":"Kobayashi Naoki","year":"2020","unstructured":"Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. 2020. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. Log. Methods Comput. Sci. 16, 4 (2020). https:\/\/lmcs.episciences.org\/6817","journal-title":"Log. Methods Comput. Sci"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In Computer Aided Verification - 23rd International Conference CAV 2011 Snowbird UT USA July 14-20 2011. Proceedings. 585\u2013591. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47 10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434313"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_15"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1093\/COMJNL\/6.4.308"},{"key":"e_1_3_1_47_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_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632879"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","unstructured":"Glen M\u00e9vel Jacques-Henri Jourdan and Fran\u00e7ois Pottier. 2019. Time Credits and Time Receipts in Iris. In Programming Languages and Systems - 28th European Symposium on Programming ESOP 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2019 Prague Czech Republic April 6-11 2019 Proceedings. 3\u201329. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_1 10.1007\/978-3-030-17184-1_1","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_1_51_1","first-page":"14","article-title":"pGCL: formal reasoning for random algorithms","volume":"22","author":"Morgan Carroll","year":"1999","unstructured":"Carroll Morgan and Annabelle McIver. 1999. pGCL: formal reasoning for random algorithms. South African Computer Journal 22 (1999), 14\u201327.","journal-title":"South African Computer Journal"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"Hiroshi Nakano. 2000. A Modality for Recursion. In 15th Annual IEEE Symposium on Logic in Computer Science Santa Barbara California USA June 26-29 2000. 255\u2013266. https:\/\/doi.org\/10.1109\/LICS.2000.855774 10.1109\/LICS.2000.855774","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"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","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01940876"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","unstructured":"Simon Spies Lennard G\u00e4her Daniel Gratzer Joseph Tassarotti Robbert Krebbers Derek Dreyer and Lars Birkedal. 2021a. Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. In PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation Virtual Event Canada June 20-25 2021. 80\u201395. https:\/\/doi.org\/10.1145\/3453483.3454031 10.1145\/3453483.3454031","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434294"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4229-9"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_28"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1236-2"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_3_1_66_1","doi-asserted-by":"crossref","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2024b. A Logical Approach to Type Soundness. (2024). https:\/\/iris-project.org\/pdfs\/2024-jacm-logical-type-soundness.pdf Manuscript.","DOI":"10.1145\/3676954"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","unstructured":"Aaron Turon Derek Dreyer and Lars Birkedal. 2013. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In ACM SIGPLAN International Conference on Functional Programming ICFP\u201913 Boston MA USA - September 25 - 27 2013. 377\u2013390. https:\/\/doi.org\/10.1145\/2500365.2500600 10.1145\/2500365.2500600","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71050-9"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"},{"key":"e_1_3_1_70_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\/3674632","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674632","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:49:57Z","timestamp":1770191397000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674632"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":69,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674632"],"URL":"https:\/\/doi.org\/10.1145\/3674632","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}