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

### License

BSD License

### Topics

- Mathematics/Probability theory
- Computer science/Semantics and reasoning

### Session Quasi_Borel_Spaces

- StandardBorel
- QuasiBorel
- Measure_QuasiBorel_Adjunction
- Binary_Product_QuasiBorel
- Product_QuasiBorel
- Binary_CoProduct_QuasiBorel
- CoProduct_QuasiBorel
- Exponent_QuasiBorel
- Probability_Space_QuasiBorel
- Monad_QuasiBorel
- Pair_QuasiBorel_Measure
- Measure_as_QuasiBorel_Measure
- Bayesian_Linear_Regression

## Cite

×

Quasi_Borel_Spaces-AFP

    @article{Quasi_Borel_Spaces-AFP,
      author  = {Michikazu Hirata and Yasuhiko Minamide and Tetsuya Sato},
      title   = {Quasi-Borel Spaces},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Quasi_Borel_Spaces.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Feb 4, 2022 : Isabelle2021-1