S-Finite Measure Monad on Quasi-Borel Spaces

Michikazu Hirata 📧 and Yasuhiko Minamide 📧

August 8, 2023


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


BSD License


Related publications

  • Hirata, M., Minamide, Y., & Sato, T. (2023). Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. Schloss Dagstuhl - Leibniz-Zentrum Für Informatik. https://doi.org/10.4230/LIPICS.ITP.2023.18

Session S_Finite_Measure_Monad