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