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

BSD License*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).