Email Gateway (Oct 11 2023 at 23:37): Email Gateway (Oct 11 2023 at 23:37):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
S-Finite Measure Monad on Quasi-Borel Spaces
by Michikazu Hirata and Yasuhiko Minamide
The s-finite measure monad on quasi-Borel spaces provides a suitable denotational model for higher-order probabilistic programs with conditioning. This entry is a formalization of the s-finite measure monad and related notions, including s-finite measures, s-finite kernels, and a proof automation for quasi-Borel spaces which is an extension of our previous entry Quasi-Borel Spaces [1]. We also implement several examples of probabilistic programs in previous works and prove their property. This work is a part of the work by Hirata, Minamide, and Sato, Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL presented at the 14th Conference on Interactive Theorem Proving (ITP2023).
https://www.isa-afp.org/entries/S_Finite_Measure_Monad.html
Enjoy!
Gerwin
[1]: https://www.isa-afp.org/entries/Quasi_Borel_Spaces.html
Last updated: Jan 04 2025 at 20:18 UTC