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).
BibTeX:	@article{Quasi_Borel_Spaces-AFP, 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

Older releases: None