Quasi-Borel Spaces

Michikazu Hirata, Yasuhiko Minamide 🌐 and Tetsuya Sato 🌐

February 3, 2022

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


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


BSD License


Session Quasi_Borel_Spaces