Quasi-Borel Spaces

 Title: Quasi-Borel Spaces Authors: Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato Submission date: 2022-02-03 Abstract: The notion of quasi-Borel spaces was introduced by Heunen et al. The theory provides a suitable denotational model for higher-order probabilistic programming languages with continuous distributions. This entry is a formalization of the theory of quasi-Borel spaces, including construction of quasi-Borel spaces (product, coproduct, function spaces), the adjunction between the category of measurable spaces and the category of quasi-Borel spaces, and the probability monad on quasi-Borel spaces. This entry also contains the formalization of the Bayesian regression presented in the work of Heunen et al. This work is a part of the work by same authors, Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL, which will be published in the proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022). BibTeX: @article{Quasi_Borel_Spaces-AFP, author = {Michikazu Hirata and Yasuhiko Minamide and Tetsuya Sato}, title = {Quasi-Borel Spaces}, journal = {Archive of Formal Proofs}, month = feb, year = 2022, note = {\url{https://isa-afp.org/entries/Quasi_Borel_Spaces.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.