**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

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

### Topics

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