{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:39:44Z","timestamp":1770284384139,"version":"3.49.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"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"}]},{"name":"Independent Research Fund Denmark","award":["2032-00134B"],"award-info":[{"award-number":["2032-00134B"]}]},{"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":[[2025,1,7]]},"abstract":"<jats:p>Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it is challenging to extend these applications to languages with recursion and computational effects such as probabilistic choice, because these features are not easily represented in constructive type theory.<\/jats:p>\n                  <jats:p>\n                    We show how to define and reason about FPC\n                    <jats:sub>\u2295<\/jats:sub>\n                    , a programming language with probabilistic choice and recursive types, in guarded type theory. We use higher inductive types to represent finite distributions and guarded recursion to model recursion. We define both operational and denotational semantics of FPC\n                    <jats:sub>\u2295<\/jats:sub>\n                    , as well as a relation between the two. The relation can be used to prove adequacy, but we also show how to use it to reason about programs up to contextual equivalence.\n                  <\/jats:p>","DOI":"10.1145\/3704884","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1417-1445","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Modelling Recursion and Probabilistic Choice in Guarded Type Theory"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4600-777X","authenticated-orcid":false,"given":"Philipp","family":"Stassen","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0386-4376","authenticated-orcid":false,"given":"Rasmus Ejlers","family":"M\u00f8gelberg","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0257-1574","authenticated-orcid":false,"given":"Maaike Annebet","family":"Zwart","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6746-2734","authenticated-orcid":false,"given":"Alejandro","family":"Aguirre","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-l_8"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571195"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005097"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.27"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571254"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_14"},{"issue":"10","key":"e_1_3_2_13_2","first-page":"3127","article-title":"Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom","volume":"4","author":"Cohen Cyril","year":"2017","unstructured":"Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mortberg. 2017. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP 4, 10 (2017), 3127\u20133170. http:\/\/collegepublications.co.uk\/ifcolog\/?00019","journal-title":"FLAP"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Rapha\u00eblle Crubill\u00e9 and Ugo Dal Lago. 2014. On Probabilistic Applicative Bisimulation and Call-by-Value A-Calculi. In Programming Languages and Systems - 23rd European Symposium on Programming ESOP 2014 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2014 Grenoble France April 5-13 2014 Proceedings (Lecture Notes in Computer Science Vol. 8410) Zhong Shao (Ed.). Springer 209\u2013228. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_12 10.1007\/978-3-642-54833-8_12","DOI":"10.1007\/978-3-642-54833-8_12"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371125"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3164540"},{"key":"e_1_3_2_18_2","volume-title":"Axiomatic domain theory in categories of partial maps","author":"Fiore Marcelo P.","year":"1994","unstructured":"Marcelo P. Fiore. 1994. Axiomatic domain theory in categories of partial maps. Ph. D. Dissertation. University of Edinburgh, UK. http:\/\/hdl.handle.net\/1842\/406"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632854"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704863"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15240-5_l"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39173"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_10"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533359"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535872"},{"key":"e_1_3_2_29_2","unstructured":"T. Lindvall. 2002. Lectures on the Coupling Method. Dover Publications Incorporated."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000087"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Rasmus Ejlers Mogelberg and Andrea Vezzosi. 2021. Two Guarded Recursive Powerdomains for Applicative Simulation. In Proceedings 37th Conference on Mathematical Foundations of Programming Semantics MFPS 2021 Hybrid: Salzburg Austria and Online 30th August - 2nd September 2021 (EPTCS Vol. 351) Ana Sokolova (Ed.). 200\u2013217. https:\/\/doi.org\/10.4204\/EPTCS.351.13 10.4204\/EPTCS.351.13","DOI":"10.4204\/EPTCS.351.13"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Rasmus Ejlers Mogelberg and Maaike Zwart. 2024. What Monads Can and Cannot Do with a Bit of Extra Time. In 32nd EACSL Annual Conference on Computer Science Logic CSL 2024 February 19-23 2024 Naples Italy (LIPIcs Vol. 288) Aniello Murano and Alexandra Silva (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 39:1-39:18. https:\/\/doi.org\/10.4230\/LIPICS.CSL.2024.39 10.4230\/LIPICS.CSL.2024.39","DOI":"10.4230\/LIPICS.CSL.2024.39"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2015.12.020"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1996.0052"},{"key":"e_1_3_2_36_2","unstructured":"Gordon D Plotkin. 1985. Denotational semantics with partial functions. Lecture at CSLI Summer School (1985)."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Jonathan Sterling Daniel Gratzer and Lars Birkedal. 2022. Denotational semantics of general store and polymorphism. CoRR abs\/2210.02169 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2210.02169 10.48550\/ARXIV.2210.02169 arXiv:2210.02169","DOI":"10.48550\/ARXIV.2210.02169"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2307.16608"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1236-2"},{"key":"e_1_3_2_40_2","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book Institute for Advanced Study."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290349"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_3_2_43_2","unstructured":"C. Villani. 2008. Optimal Transport: Old and New. Springer Berlin Heidelberg."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_2_46_2","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\/3704884","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704884","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:08Z","timestamp":1770200048000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704884"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":45,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704884"],"URL":"https:\/\/doi.org\/10.1145\/3704884","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}