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).
  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.