{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:21Z","timestamp":1747173441147,"version":"3.40.5"},"reference-count":49,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2021,12,7]],"date-time":"2021-12-07T00:00:00Z","timestamp":1638835200000},"content-version":"unspecified","delay-in-days":189,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We give two geometry of interaction models for a typed \u03bb-calculus with recursion endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The models are based on the category of measurable spaces and partial measurable functions, and the category of measurable spaces and s-finite kernels, respectively. The former is proved adequate with respect to both a distribution-based and a sampling-based operational semantics, while the latter is proved adequate with respect to a sampling-based operational semantics.<\/jats:p>","DOI":"10.1017\/s0960129521000396","type":"journal-article","created":{"date-parts":[[2021,12,7]],"date-time":"2021-12-07T07:19:31Z","timestamp":1638861571000},"page":"633-681","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["The geometry of Bayesian programming"],"prefix":"10.1017","volume":"31","author":[{"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2647-0310","authenticated-orcid":false,"given":"Naohiko","family":"Hoshino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2021,12,7]]},"reference":[{"key":"S0960129521000396_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837672"},{"volume-title":"Cambridge Tracts in Theoretical Computer Science","year":"2016","author":"Jacobs","key":"S0960129521000396_ref29"},{"key":"S0960129521000396_ref16","doi-asserted-by":"crossref","unstructured":"Dal Lago, U. , Sangiorgi, D. and Alberti, M. (2014). On coinductive equivalences for higher-order probabilistic functional programs. In: Proceedings of POPL 2014, 297\u2013308.","DOI":"10.1145\/2578855.2535872"},{"key":"S0960129521000396_ref20","first-page":"1","article-title":"Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming","volume":"2","author":"Ehrhard","year":"2018","journal-title":"PACMPL"},{"volume-title":"A Survey of Graphical Languages for Monoidal Categories","year":"2011","author":"Selinger","key":"S0960129521000396_ref44"},{"key":"S0960129521000396_ref37","doi-asserted-by":"publisher","DOI":"10.1063\/1.1699114"},{"key":"S0960129521000396_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80216-6"},{"key":"S0960129521000396_ref48","unstructured":"Wood, F. D. , van de Meent, J. and Mansinghka, V. (2014). A new approach to probabilistic programming inference. In: Proceedings of AISTATS 2014, 1024\u20131032."},{"key":"S0960129521000396_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80398-6"},{"volume-title":"London Mathematical Society Lecture Note Series","year":"1995","author":"Lafont","key":"S0960129521000396_ref34"},{"key":"S0960129521000396_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/3164540"},{"key":"S0960129521000396_ref26","doi-asserted-by":"crossref","unstructured":"Hoshino, N. , Muroya, K. and Hasuo, I. (2014). Memoryful geometry of interaction: From coalgebraic components to algebraic effects. In: Proceedings of CSL-LICS 2014.","DOI":"10.1145\/2603088.2603124"},{"key":"S0960129521000396_ref42","doi-asserted-by":"publisher","DOI":"10.1016\/0022-314X(80)90084-0"},{"key":"S0960129521000396_ref46","doi-asserted-by":"crossref","unstructured":"V\u00e1k\u00e1r, M. , Kammar, O. and Staton, S. (2019). A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages 3 (POPL) 36:1\u201336:29.","DOI":"10.1145\/3290349"},{"key":"S0960129521000396_ref24","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/57.1.97"},{"key":"S0960129521000396_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(76)80043-8"},{"key":"S0960129521000396_ref13","doi-asserted-by":"crossref","unstructured":"Dal Lago, U. and Grellois, C. (2017). Probabilistic termination by monadic affine sized typing. In: Proceedings of ESOP 2017, 393\u2013419.","DOI":"10.1007\/978-3-662-54434-1_15"},{"key":"S0960129521000396_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.02.001"},{"key":"S0960129521000396_ref27","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"S0960129521000396_ref10","unstructured":"Clairambault, P. and Paquet, H. (2018). Fully abstract models of the probabilistic lambda-calculus. In: Proceedings of CSL 2018, 16:1\u201316:17."},{"volume-title":"Probability and Measure","year":"1986","author":"Billingsley","key":"S0960129521000396_ref5"},{"key":"S0960129521000396_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.11.016"},{"key":"S0960129521000396_ref31","unstructured":"Jones, C. (1990). Probabilistic Non-Determinism. PhD thesis, University of Edinburgh."},{"key":"S0960129521000396_ref35","doi-asserted-by":"crossref","unstructured":"Laurent, O. (2001). A token machine for full geometry of interaction. In: Proceedings of TLCA 2001, 283\u2013297.","DOI":"10.1007\/3-540-45413-6_23"},{"key":"S0960129521000396_ref25","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"S0960129521000396_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209187"},{"key":"S0960129521000396_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100074338"},{"key":"S0960129521000396_ref4","first-page":"781","article-title":"PRIMES is in P","volume":"2","author":"Agrawal","year":"2002","journal-title":"Annals of Mathematics"},{"key":"S0960129521000396_ref43","article-title":"Formal verification of higher-order probabilistic programs: Reasoning about approximation, convergence, Bayesian inference, and optimization","volume":"3","author":"Sato","year":"2019","journal-title":"PACMPL"},{"key":"S0960129521000396_ref47","doi-asserted-by":"crossref","unstructured":"Wand, M. , Culpepper, R. , Giannakopoulos, T. and Cobb, A. (2018). Contextual equivalence for a probabilistic language with continuous random variables and recursion. Proceedings of the ACM on Programming Languages 2 (ICFP) 87:1\u201387:30.","DOI":"10.1145\/3236782"},{"key":"S0960129521000396_ref23","unstructured":"Goodman, N. D. , Mansinghka, V. K. , Roy, D. M. , Bonawitz, K. and Tenenbaum, J. B. (2008). Church: A language for generative models. In: Proceedings of UAI 2008, 220\u2013229."},{"key":"S0960129521000396_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199483"},{"key":"S0960129521000396_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_12"},{"key":"S0960129521000396_ref30","doi-asserted-by":"crossref","unstructured":"Jacobs, B. , Zanasi, F. and Kissinger, A. (2018). Causal inference by string diagram surgery. arXiv:1811.08338 [cs.LO].","DOI":"10.1007\/978-3-030-17127-8_18"},{"key":"S0960129521000396_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129521000396_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00241-9"},{"key":"S0960129521000396_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003730"},{"key":"S0960129521000396_ref9","unstructured":"Cho, K. and Jacobs, B. (2017). Disintegration and bayesian inversion, both abstractly and concretely. to appear in Mathematical Structures in Computer Science."},{"key":"S0960129521000396_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"S0960129521000396_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"S0960129521000396_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951942"},{"key":"S0960129521000396_ref2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"S0960129521000396_ref12","doi-asserted-by":"crossref","unstructured":"Dal Lago, U. , Faggian, C. , Valiron, B. and Yoshimizu, A. (2017). The geometry of parallelism: classical, probabilistic, and quantum effects. In: Proceedings of POPL 2017, 833\u2013845.","DOI":"10.1145\/3093333.3009859"},{"key":"S0960129521000396_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/507382.507385"},{"key":"S0960129521000396_ref15","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785663"},{"key":"S0960129521000396_ref7","unstructured":"Breuvart, F. and Dal Lago, U. (2018). On intersection types and probabilistic lambda calculi. In: Proceedings of PPDP 2018, 8:1\u20138:13."},{"key":"S0960129521000396_ref14","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785663"},{"key":"#cr-split#-S0960129521000396_ref39.1","doi-asserted-by":"crossref","unstructured":"Moggi, E. (1991). Notions of computation and monads. Information and Computation 93","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"#cr-split#-S0960129521000396_ref39.2","unstructured":"(1) 55-92. Selections from 1989 IEEE Symposium on Logic in Computer Science."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000396","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,31]],"date-time":"2022-01-31T11:37:22Z","timestamp":1643629042000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000396\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6]]},"references-count":49,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,6]]}},"alternative-id":["S0960129521000396"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000396","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2021,6]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}