{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:51Z","timestamp":1780994691199,"version":"3.54.1"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>Developing denotational models for higher-order languages that combine  \nprobabilistic and nondeterministic choice is known to be very  \nchallenging. In this paper, we propose an alternative approach based  \non operational techniques. We study a higher-order language combining  \nparametric polymorphism, recursive types, discrete probabilistic choice  \nand countable nondeterminism. We define probabilistic generalizations  \nof may- and must-termination as the optimal and pessimal probabilities  \nof termination. Then we define step-indexed logical relations and show  \nthat they are sound and complete with respect to the induced contextual  \npreorders. For may-equivalence we use step-indexing over the natural  \nnumbers whereas for must-equivalence we index over the countable  \nordinals. We then show than the probabilities of may- and  \nmust-termination coincide with the maximal and minimal probabilities of  \ntermination under all schedulers. Finally we derive the equational  \ntheory induced by contextual equivalence and show that it validates the  \ndistributive combination of the algebraic theories for probabilistic  \nand nondeterministic choice.<\/jats:p>","DOI":"10.1145\/3571195","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"33-60","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6746-2734","authenticated-orcid":false,"given":"Alejandro","family":"Aguirre","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"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, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1215\/ijm\/1255631584"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/lmcs-9(4:4)2013"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.107"},{"key":"e_1_2_1_7_1","volume-title":"Foundations of Software Science and Computation Structures","author":"Bizjak Ale\u0161","unstructured":"Ale\u0161 Bizjak and Lars Birkedal . 2015. Step-Indexed Logical Relations for Probability . In Foundations of Software Science and Computation Structures , Andrew Pitts (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 279\u2013294. isbn:978-3-662-46678-0 Ale\u0161 Bizjak and Lars Birkedal. 2015. Step-Indexed Logical Relations for Probability. In Foundations of Software Science and Computation Structures, Andrew Pitts (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 279\u2013294. isbn:978-3-662-46678-0"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2017.23"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2019.8785673"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951942"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2010.364"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_13"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.64"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158147"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(1:3)2019"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535865"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394795"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2017.8005137"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics52264.2021.9470678"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.1989.39173"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/s1571-0661(05)80216-6"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_26_1","volume-title":"Set Theory","author":"Kunen Kenneth","year":"1848","unstructured":"Kenneth Kunen . 2011. Set Theory . College Publications . isbn:978 1848 900509 Kenneth Kunen. 2011. Set Theory. College Publications. isbn:9781848900509"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_28_1","unstructured":"S\u00f8ren B\u00f8gh Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. BRICS. https:\/\/www.brics.dk\/DS\/98\/2\/BRICS-DS-98-2.pdf \t\t\t\t  S\u00f8ren B\u00f8gh Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. BRICS. https:\/\/www.brics.dk\/DS\/98\/2\/BRICS-DS-98-2.pdf"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics52264.2021.9470717"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.28"},{"key":"e_1_2_1_31_1","volume-title":"Nondeterminism and Probabilistic Choice: Obeying the Laws. In CONCUR 2000 \u2014 Concurrency Theory, Catuscia Palamidessi (Ed.). Springer Berlin Heidelberg","author":"Mislove Michael","year":"2000","unstructured":"Michael Mislove . 2000 . Nondeterminism and Probabilistic Choice: Obeying the Laws. In CONCUR 2000 \u2014 Concurrency Theory, Catuscia Palamidessi (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 350\u2013365. isbn:978-3-540-44618-7 Michael Mislove. 2000. Nondeterminism and Probabilistic Choice: Obeying the Laws. In CONCUR 2000 \u2014 Concurrency Theory, Catuscia Palamidessi (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 350\u2013365. isbn:978-3-540-44618-7"},{"key":"e_1_2_1_32_1","unstructured":"Carroll Morgan and Annabelle McIver. 1999. pGCL: Formal reasoning for random algorithms. \t\t\t\t  Carroll Morgan and Annabelle McIver. 1999. pGCL: Formal reasoning for random algorithms."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/1104.003.0011"},{"key":"e_1_2_1_35_1","volume-title":"Higher Order Operational Techniques in Semantics","author":"Pitts Andrew","unstructured":"Andrew Pitts and Ian Stark . 1998. Operational Reasoning for Functions with Local State . In Higher Order Operational Techniques in Semantics , Andrew Gordon and Andrew Pitts (Eds.). Publications of the Newton Institute, Cambridge University Press , 227\u2013273. http:\/\/www.inf.ed.ac.uk\/~stark\/operfl.html Andrew Pitts and Ian Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics, Andrew Gordon and Andrew Pitts (Eds.). Publications of the Newton Institute, Cambridge University Press, 227\u2013273. http:\/\/www.inf.ed.ac.uk\/~stark\/operfl.html"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205035"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90003-1"},{"key":"e_1_2_1_38_1","volume-title":"Probability and Nondeterminism in Operational Models of Concurrency. In CONCUR 2006 \u2013 Concurrency Theory, Christel Baier and Holger Hermanns (Eds.). Springer Berlin Heidelberg","author":"Segala Roberto","year":"2006","unstructured":"Roberto Segala . 2006 . Probability and Nondeterminism in Operational Models of Concurrency. In CONCUR 2006 \u2013 Concurrency Theory, Christel Baier and Holger Hermanns (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 64\u201378. isbn:978-3-540-37377-3 Roberto Segala. 2006. Probability and Nondeterminism in Operational Models of Concurrency. In CONCUR 2006 \u2013 Concurrency Theory, Christel Baier and Holger Hermanns (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 64\u201378. isbn:978-3-540-37377-3"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429111"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290349"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0960129505005074"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the 17th International conference on Artificial Intelligence and Statistics. 1024\u20131032","author":"Wood Frank","unstructured":"Frank Wood , Jan Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference . In Proceedings of the 17th International conference on Artificial Intelligence and Statistics. 1024\u20131032 . Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference. In Proceedings of the 17th International conference on Artificial Intelligence and Statistics. 1024\u20131032."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/645835.670408"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498677"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571195","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571195","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571195"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571195"],"URL":"https:\/\/doi.org\/10.1145\/3571195","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}