### Abstract

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

### License

BSD License

### Topics

- Computer science/Semantics and reasoning
- Mathematics/Measure and integration
- Mathematics/Probability theory

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

- Lemmas_S_Finite_Measure_Monad
- Kernels
- QuasiBorel
- QBS_Morphism
- Measure_QuasiBorel_Adjunction
- Monad_QuasiBorel
- Montecarlo
- Query

### Depends on

- Standard Borel Spaces

### Used by

- Disintegration Theorem

### Auto-related entries

- Quasi-Borel Spaces
- Automated Stateful Protocol Verification
- Proof Strategy Language

## Cite

×

S_Finite_Measure_Monad-AFP

    @article{S_Finite_Measure_Monad-AFP,
      author  = {Michikazu Hirata and Yasuhiko Minamide},
      title   = {S-Finite Measure Monad on Quasi-Borel Spaces},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/S_Finite_Measure_Monad.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest