{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T16:49:06Z","timestamp":1756572546214,"version":"3.40.5"},"reference-count":46,"publisher":"Cambridge University Press (CUP)","issue":"10","license":[{"start":{"date-parts":[[2021,8,13]],"date-time":"2021-08-13T00:00:00Z","timestamp":1628812800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial <jats:italic>\u03c3<\/jats:italic>-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies, we define valuations and lower integrals on sets and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed.<\/jats:p>","DOI":"10.1017\/s0960129521000165","type":"journal-article","created":{"date-parts":[[2021,8,13]],"date-time":"2021-08-13T12:27:31Z","timestamp":1628857651000},"page":"1301-1329","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Synthetic topology in Homotopy Type Theory for probabilistic programming"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2238-8731","authenticated-orcid":false,"given":"Martin E.","family":"Bidlingmaier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5792-0658","authenticated-orcid":false,"given":"Florian","family":"Faissole","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2802-0973","authenticated-orcid":false,"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2021,8,13]]},"reference":[{"key":"S0960129521000165_ref2","doi-asserted-by":"crossref","unstructured":"Altenkirch, T. , Danielsson, N. A. and Kraus, N. (2017). Partiality, revisited - the partiality monad as a quotient inductive-inductive type. In: FOSSACS 2017, 534\u2013549.","DOI":"10.1007\/978-3-662-54458-7_31"},{"key":"S0960129521000165_ref41","unstructured":"Sterling, J. , Angiuli, C. and Gratzer, D. (2020). A cubical language for bishop sets. arXiv preprint arXiv:2003.01491."},{"key":"S0960129521000165_ref23","unstructured":"Huang, D. (2017). On Programming Languages for Probabilistic Modeling. PhD thesis, Harvard (2017)."},{"key":"S0960129521000165_ref3","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-3-319-89366-2_16","volume-title":"International Conference on Foundations of Software Science and Computation Structures","author":"Altenkirch","year":"2018"},{"key":"S0960129521000165_ref20","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/BFb0092872","volume-title":"Categorical Aspects of Topology and Analysis","author":"Giry","year":"1982"},{"key":"S0960129521000165_ref24","doi-asserted-by":"crossref","unstructured":"Huang, D. , Morrisett, G. and Spitters, B. (2020). An application of computable distributions to the semantics of probabilistic programs. In: Barthe, G. , Silva, A. and Katoen, J.-P. (eds.), Foundations of Probabilistic Programming.","DOI":"10.1017\/9781108770750.004"},{"key":"S0960129521000165_ref15","unstructured":"Escard\u00f3, M. H. and Knapp, C. M. (2017). Partial elements and recursion via dominances in univalent type theory. In: Goranko, V. and Dam, M. (eds.), CSL 2017, vol. 82. LIPIcs. Schloss Dagstuhl, 21:1\u201321:16. ISBN 978-3-95977-045-3."},{"key":"S0960129521000165_ref33","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","article-title":"Notions of computation and monads","volume":"93","author":"Moggi","year":"1991","journal-title":"Information and Computation"},{"key":"S0960129521000165_ref10","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1007\/s001530100123","article-title":"Metric boolean algebras and constructive measure theory","volume":"41","author":"Coquand","year":"2002","journal-title":"Archive for Mathematical Logic"},{"key":"S0960129521000165_ref38","unstructured":"Shulman, M. (2019). All (\u221e,1) -Toposes have Strict Univalent Universes."},{"key":"S0960129521000165_ref16","unstructured":"Faissole, F. and Spitters, B. (2018). Preuves constructives de programmes probabilistes. In: Presentation at JFLA 2018 - Journ\u00e9es Francophones des Langages Applicatifs. https:\/\/hal.inria.fr\/hal-01654459"},{"key":"S0960129521000165_ref44","doi-asserted-by":"crossref","first-page":"908","DOI":"10.2307\/2274144","article-title":"On choice sequences determined by spreads","volume":"49","author":"Van Der Hoeven","year":"1984","journal-title":"The Journal of Symbolic Logic"},{"key":"S0960129521000165_ref31","unstructured":"Lumsdaine, P. and Shulman, M. (2017). Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society 1\u201350."},{"key":"S0960129521000165_ref8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511565663","volume-title":"Varieties of Constructive Mathematics","author":"Bridges","year":"1987"},{"key":"S0960129521000165_ref36","unstructured":"Rosolini, G. (1986). Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford."},{"key":"S0960129521000165_ref12","doi-asserted-by":"crossref","unstructured":"Coquand, T. , Mannaa, B. and Ruch, F. (2017). Stack semantics of type theory. In: 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 1\u201311.","DOI":"10.1109\/LICS.2017.8005130"},{"key":"S0960129521000165_ref11","first-page":"1","article-title":"Integrals and valuations","volume":"1","author":"Coquand","year":"2009","journal-title":"Journal of Logic and Analysis"},{"key":"S0960129521000165_ref1","doi-asserted-by":"crossref","unstructured":"Altenkirch, T. , McBride, C. and Swierstra, W. (2007). Observational equality, now! In: Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification, PLPV 2007. ACM, 57\u201368. ISBN 9781595936776.","DOI":"10.1145\/1292597.1292608"},{"key":"S0960129521000165_ref5","doi-asserted-by":"crossref","unstructured":"Audebaud, P. and Paulin-Mohring, C. (2006). Proofs of randomized algorithms in Coq. In: MPC.","DOI":"10.1007\/11783596_6"},{"key":"S0960129521000165_ref39","first-page":"1","article-title":"Type classes for mathematics in type theory","volume":"21","author":"Spitters","year":"2011","journal-title":"MSCS, special issue on \u2018Interactive Theorem Proving and the Formalization of Mathematics\u2019"},{"key":"S0960129521000165_ref37","doi-asserted-by":"crossref","first-page":"856","DOI":"10.1017\/S0960129517000147","article-title":"Brouwer\u2019s fixed-point theorem in real-cohesive homotopy type theory","volume":"28","author":"Shulman","year":"2018","journal-title":"Mathematical Structures in Computer Science"},{"key":"S0960129521000165_ref4","unstructured":"Anel, M. (2020). Computing enveloping \u221e-topoi. href http:\/\/mathieu.anel.free.fr\/mat\/doc\/Anel-2020-MURImeeting.pdf"},{"key":"S0960129521000165_ref13","first-page":"21","article-title":"Synthetic topology: of data types and classical spaces","volume":"87","author":"Escard\u00f3","year":"2004","journal-title":"ENTCS"},{"key":"S0960129521000165_ref32","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1137\/1006063","article-title":"A convenient method for generating normal variables","volume":"6","author":"Marsaglia","journal-title":"SIAM Review"},{"key":"S0960129521000165_ref25","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/BFb0084217","volume-title":"Category Theory","author":"Hyland","year":"1991"},{"key":"S0960129521000165_ref30","unstructured":"Le\u0161nik, D. (2010). Synthetic Topology and Constructive Metric Spaces. Diss. University of Ljubljana."},{"key":"S0960129521000165_ref35","doi-asserted-by":"crossref","unstructured":"Rijke, E. and Spitters, B. (2014). Sets in homotopy type theory. In: MSCS, Special Issue: From Type Theory and Homotopy Theory to Univalent Foundations.","DOI":"10.1017\/S0960129514000553"},{"key":"S0960129521000165_ref26","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1112\/plms\/s3-38.2.237","article-title":"On a topological topos","volume":"3","author":"Johnstone","year":"1979","journal-title":"Proceedings of the London Mathematical Society"},{"volume-title":"Homotopy Type Theory: Univalent Foundations for Mathematics","year":"2013","key":"S0960129521000165_ref43"},{"key":"S0960129521000165_ref6","doi-asserted-by":"crossref","unstructured":"Bauer, A. , Gross, J. , Lumsdaine, P. L. , Shulman, M. , Sozeau, M. and Spitters, B. (2017). The HoTT library: A formalization of homotopy type theory in coq. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017. ACM, 164\u2013172. ISBN 978-1-4503-4705-1.","DOI":"10.1145\/3018610.3018615"},{"key":"S0960129521000165_ref28","unstructured":"Jones, C. and Plotkin, G. (1989). A probabilistic powerdomain of evaluations. In: LICS."},{"key":"S0960129521000165_ref14","doi-asserted-by":"crossref","first-page":"770","DOI":"10.1016\/j.apal.2016.04.011","article-title":"A constructive manifestation of the Kleene\u2013Kreisel continuous functionals","volume":"167","author":"Escard\u00f3","year":"2016","journal-title":"Annals of Pure and Applied Logic"},{"key":"S0960129521000165_ref17","doi-asserted-by":"crossref","unstructured":"Fourman, M. (1984). Continuous truth I: Non-constructive objects. In: Studies in Logic and the Foundations of Mathematics, vol. 112. Elsevier, 161\u2013180.","DOI":"10.1016\/S0049-237X(08)71816-0"},{"key":"S0960129521000165_ref45","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1002\/malq.200710028","article-title":"A localic theory of lower and upper integrals","volume":"54","author":"Vickers","year":"2008","journal-title":"Mathematical Logic Quarterly"},{"key":"S0960129521000165_ref9","unstructured":"Coquand, T. (2019). Constructive Mathematics and Higher Topos Theory. http:\/\/www.cse.chalmers.se\/coquand\/birmingham.pdf"},{"key":"S0960129521000165_ref29","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/j.entcs.2008.10.013","article-title":"Presenting dcpos and dcpo algebras","volume":"218","author":"Jung","year":"2008","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"S0960129521000165_ref21","doi-asserted-by":"crossref","unstructured":"Heunen, C. , Kammar, O. , Staton, S. and Yang, H. (2017). A convenient category for higher-order probability theory. In: 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), 1\u201312.","DOI":"10.1109\/LICS.2017.8005137"},{"key":"S0960129521000165_ref19","doi-asserted-by":"crossref","unstructured":"Gilbert, G. (2016). Formalising real numbers in homotopy type theory. In: CPP 2017.","DOI":"10.1145\/3018610.3018614"},{"key":"S0960129521000165_ref42","unstructured":"Swan, A. and Uemura, T. (2019). On Church\u2019s thesis in cubical assemblies. arXiv preprint arXiv:1905.03014."},{"key":"S0960129521000165_ref7","unstructured":"B\u00e9guelin, S. Z. (2010). Formal Certification of Game-Based Cryptographic Proofs. PhD thesis, Ecole Nationale des Mines de Paris."},{"key":"S0960129521000165_ref22","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1090\/S0002-9947-1948-0028922-8","article-title":"Measures in Boolean algebras","volume":"64","author":"Horn","year":"1948","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0960129521000165_ref46","unstructured":"Vickers, S. (2011). A Monad of Valuation Locales. http:\/\/www.cs.bham.ac.uk\/sjv\/Riesz.pdf"},{"key":"S0960129521000165_ref18","doi-asserted-by":"crossref","unstructured":"Fourman, M. (2013). Continuous truth II: Reflections. In: WoLLIC.","DOI":"10.1007\/978-3-642-39992-3_15"},{"key":"S0960129521000165_ref34","first-page":"1","volume-title":"International Conference on Foundations of Software Science and Computation Structures","author":"Plotkin","year":"2001"},{"volume-title":"Sketches of an Elephant: A Topos Theory Compendium","year":"2002","author":"Johnstone","key":"S0960129521000165_ref27"},{"key":"S0960129521000165_ref40","doi-asserted-by":"crossref","unstructured":"Staton, S. , Yang, H. , Heunen, C. , Kammar, O. and Wood, F. (2016). Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. CoRR, abs\/1601.04943.","DOI":"10.1145\/2933575.2935313"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000165","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,28]],"date-time":"2022-09-28T10:14:29Z","timestamp":1664360069000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000165\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,13]]},"references-count":46,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2021,11]]}},"alternative-id":["S0960129521000165"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000165","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2021,8,13]]},"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"}}]}}