{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:21Z","timestamp":1767929481077,"version":"3.49.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1637532"],"award-info":[{"award-number":["1637532"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["ProfoundNet"],"award-info":[{"award-number":["ProfoundNet"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/P010040\/1"],"award-info":[{"award-number":["EP\/P010040\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2020,1]]},"abstract":"<jats:p>We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs a la Scott through the use of ordered Banach spaces which allow definitions in terms of fixed points. Our semantics is a model of intuitionistic linear logic: it is based on a symmetric monoidal closed category of ordered Banach spaces which treats randomness as a linear resource, but by constructing an exponential comonad we can also accommodate non-linear reasoning. We apply our semantics to the verification of the classical Gibbs sampling algorithm.<\/jats:p>","DOI":"10.1145\/3371125","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Semantics of higher-order probabilistic programs with conditioning"],"prefix":"10.1145","volume":"4","author":[{"given":"Fredrik","family":"Dahlqvist","sequence":"first","affiliation":[{"name":"University College London, UK \/ Imperial College London, UK"}]},{"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(98)00106-6"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"C. Aliprantis and K. Border. 1999. Infinite dimensional analysis. Vol. 32006. Springer.  C. Aliprantis and K. Border. 1999. Infinite dimensional analysis. Vol. 32006. Springer.","DOI":"10.1007\/978-3-662-03961-8"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"C. D. Aliprantis and O. Burkinshaw. 2006. Positive operators. Vol. 119. Springer Science &amp; Business Media.  C. D. Aliprantis and O. Burkinshaw. 2006. Positive operators. Vol. 119. Springer Science &amp; Business Media.","DOI":"10.1007\/978-1-4020-5008-4"},{"key":"e_1_2_2_4_1","volume-title":"ACM SIGPLAN Notices","volume":"51","author":"Borgstr\u00f6m J."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1111\/1467-9574.00056"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2537948"},{"key":"e_1_2_2_7_1","volume-title":"FOSSACS 2017. Proceedings.","author":"Clerc F."},{"key":"e_1_2_2_8_1","volume-title":"International Conference on Foundations of Software Science and Computation Structures. Springer, 20\u201335","author":"Crubill\u00e9 R."},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"F. Dahlqvist V. Danos I. Garnier and A. Silva. 2018. Borel kernels and their Approximations Categorically. In Mathematical Foundations of Programming Semantics (MFPS).  F. Dahlqvist V. Danos I. Garnier and A. Silva. 2018. Borel kernels and their Approximations Categorically. In Mathematical Foundations of Programming Semantics (MFPS).","DOI":"10.1016\/j.entcs.2018.11.006"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1968-0222604-8"},{"key":"e_1_2_2_11_1","volume-title":"Sur les espaces de K\u00f6the. Jour. d\u2019Analyse Math. 1, 1","author":"Dieudonn\u00e9 J.","year":"1951"},{"key":"e_1_2_2_12_1","unstructured":"N. Dunford J. T. Schwartz W. G Bade and R. G. Bartle. 1971. Linear operators I. Wiley-interscience New York.  N. Dunford J. T. Schwartz W. G Bade and R. G. Bartle. 1971. Linear operators I. Wiley-interscience New York."},{"key":"e_1_2_2_13_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL","author":"Ehrhard T.","year":"2017"},{"key":"e_1_2_2_14_1","volume-title":"ACM SIGPLAN Notices","volume":"49","author":"Ehrhard T."},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"T. Eisner B. Farkas M. Haase and R. Nagel. 2015. Operator theoretic aspects of ergodic theory. Vol. 272. Springer.  T. Eisner B. Farkas M. Haase and R. Nagel. 2015. Operator theoretic aspects of ergodic theory. Vol. 272. Springer.","DOI":"10.1007\/978-3-319-16898-2"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.2307\/2373758"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01344164"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"S. Geman and D. Geman. 1987. Stochastic relaxation Gibbs distributions and the Bayesian restoration of images. In Readings in computer vision. Elsevier 564\u2013584.  S. Geman and D. Geman. 1987. Stochastic relaxation Gibbs distributions and the Bayesian restoration of images. In Readings in computer vision. Elsevier 564\u2013584.","DOI":"10.1016\/B978-0-08-051581-6.50057-X"},{"key":"e_1_2_2_19_1","volume-title":"Categorical aspects of topology and analysis","author":"Giry M."},{"key":"e_1_2_2_20_1","doi-asserted-by":"crossref","volume-title":"Produits tensoriels topologiques et espaces nucl\u00e9aires","author":"Grothendieck A.","DOI":"10.1090\/memo\/0016"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1511\/2001.28.3336"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"O. Heunen C.and Kammar S. Staton and H. Yang. 2017. A convenient category for higher-order probability theory. In LICS. IEEE 1\u201312.  O. Heunen C.and Kammar S. Staton and H. Yang. 2017. A convenient category for higher-order probability theory. In LICS. IEEE 1\u201312.","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_2_2_23_1","volume-title":"Classical descriptive set theory. Graduate Text in Mathematics","author":"Kechris A. S."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"D. Licata and E. Finster. 2014. Eilenberg-MacLane spaces in homotopy type theory. In LICS. ACM 66.  D. Licata and E. Finster. 2014. Eilenberg-MacLane spaces in homotopy type theory. In LICS. ACM 66.","DOI":"10.1145\/2603088.2603153"},{"key":"e_1_2_2_27_1","volume-title":"Categorical semantics of linear logic. Panoramas et syntheses 27","author":"Mellies P.","year":"2009"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000426"},{"key":"e_1_2_2_29_1","first-page":"279","article-title":"An exponential law for regular ordered Banach spaces","volume":"24","author":"Min K. C.","year":"1983","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","volume-title":"Introduction to tensor products of Banach spaces","author":"Ryan R. A.","DOI":"10.1007\/978-1-4471-3903-4"},{"key":"e_1_2_2_31_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL","author":"\u015acibior A.","year":"2017"},{"key":"e_1_2_2_32_1","volume-title":"International Conference on Foundations of Software Science and Computational Structures. Springer, 81\u201396","author":"Selinger P."},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","volume-title":"Commutative semantics for probabilistic programming","author":"Staton S.","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"e_1_2_2_34_1","volume-title":"2016 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 1\u201310","author":"Staton S."},{"key":"e_1_2_2_35_1","volume-title":"Proceedings of the ACM on Programming Languages 3, POPL","author":"V\u00e1k\u00e1r M.","year":"2019"},{"key":"e_1_2_2_36_1","volume-title":"Positivity","author":"Wickstead A. W."},{"key":"e_1_2_2_37_1","volume-title":"Foundations of quantum mechanics and ordered linear spaces","author":"Wittstock G."},{"key":"e_1_2_2_38_1","unstructured":"Y. Wong and K. Ng. 1973. Partially ordered topological vector spaces. Oxford University Press.  Y. Wong and K. Ng. 1973. Partially ordered topological vector spaces. Oxford University Press."},{"key":"e_1_2_2_39_1","doi-asserted-by":"crossref","volume-title":"Introduction to operator theory in Riesz spaces","author":"Zaanen A. C.","DOI":"10.1007\/978-3-642-60637-3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371125","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371125","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371125","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371125"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371125"],"URL":"https:\/\/doi.org\/10.1145\/3371125","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}