Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL

Authors Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato

Thumbnail PDF


  • Filesize: 0.81 MB
  • 18 pages

Document Identifiers

Author Details

Michikazu Hirata
  • School of Computing, Tokyo Institute of Technology, Japan
Yasuhiko Minamide
  • School of Computing, Tokyo Institute of Technology, Japan
Tetsuya Sato
  • School of Computing, Tokyo Institute of Technology, Japan

Cite AsGet BibTex

Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Higher-order probabilistic programs are used to describe statistical models and machine-learning mechanisms. The programming languages for them are equipped with three features: higher-order functions, sampling, and conditioning. In this paper, we propose an Isabelle/HOL library for probabilistic programs supporting all of those three features. We extend our previous quasi-Borel theory library in Isabelle/HOL. As a basis of the theory, we formalize s-finite kernels, which is considered as a theoretical foundation of first-order probabilistic programs and a key to support conditioning of probabilistic programs. We also formalize the Borel isomorphism theorem which plays an important role in the quasi-Borel theory. Using them, we develop the s-finite measure monad on quasi-Borel spaces. Our extension enables us to describe higher-order probabilistic programs with conditioning directly as an Isabelle/HOL term whose type is that of morphisms between quasi-Borel spaces. We also implement the qbs prover for checking well-typedness of an Isabelle/HOL term as a morphism between quasi-Borel spaces. We demonstrate several verification examples of higher-order probabilistic programs with conditioning.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Mathematics of computing → Probabilistic algorithms
  • Higher-order probabilistic program
  • s-finite kernel
  • Quasi-Borel spaces
  • Isabelle/HOL


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Reynald Affeldt, Cyril Cohen, and Ayumu Saito. Semantics of probabilistic programs using s-finite kernels in Coq. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 3-16, New York, NY, USA, 2023. Association for Computing Machinery. URL:
  2. Robert J. Aumann. Borel structures for function spaces. Illinois Journal of Mathematics, 5(4):614-630, 1961. URL:
  3. Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389-423, 2017. URL:
  4. Alexander Bagnall and Gordon Stewart. Certifying the true error: Machine learning in Coq with verified generalization guarantees. Proceedings of the AAAI Conference on Artificial Intelligence, 33:2662-2669, 2019. URL:
  5. David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar, Sefidgar. CryptHOL: Game-based proofs in higher-order logic. Journal of Cryptology, 33:494-566, 2020. Google Scholar
  6. Marek Biskup. Lecture note of math245b in UCLA., 2020. Accessed: January 17. 2023.
  7. Manuel Eberl, Johannes Hölzl, and Tobias Nipkow. A verified compiler for probability density functions. In European Symposium on Programming (ESOP 2015), volume 9032 of LNCS, pages 80-104. Springer, 2015. URL:
  8. Michèle Giry. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, pages 68-85, Berlin, Heidelberg, 1982. Springer Berlin Heidelberg. URL:
  9. Noah D. Goodman et al. Church: a language for generative models. In UAI 2008, Proceedings of the 24th Conference in Uncertainty in Artificial Intelligence, pages 220-229. AUAI Press, 2008. Google Scholar
  10. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017. IEEE Press, 2017. URL:
  11. Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. Program logic for higher-order probabilistic programs in Isabelle/HOL. In Michael Hanus and Atsushi Igarashi, editors, Functional and Logic Programming, pages 57-74, Cham, 2022. Springer International Publishing. Google Scholar
  12. Johannes Hölzl. Markov processes in Isabelle/HOL. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 100-111. Association for Computing Machinery, 2017. URL:
  13. Johannes Hölzl, Armin Heller, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk. Three chapters of measure theory in Isabelle/HOL. In Interactive Theorem Proving, ITP 2011, pages 135-151. Springer Berlin Heidelberg, 2011. Google Scholar
  14. Cezary Kaliszyk and Christian Urban. Quotients revisited for Isabelle/HOL. In Proceedings of the 2011 ACM Symposium on Applied Computing, SAC, pages 1639-1644, New York, NY, USA, 2011. Association for Computing Machinery. URL:
  15. Ondřej Kunčar and Andrei Popescu. From types to sets by local type definitions in higher-order logic. In Jasmin Christian Blanchette and Stephan Merz, editors, Interactive Theorem Proving, pages 200-218, Cham, 2016. Springer International Publishing. Google Scholar
  16. Andreas Lochbihler. Probabilistic functions and cryptographic oracles in higher order logic. In Programming Languages and Systems, pages 503-531, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. URL:
  17. Mihails Milehins. An extension of the framework types-to-sets for Isabelle/HOL. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, pages 180-196, New York, NY, USA, 2022. Association for Computing Machinery. URL:
  18. Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Berlin, Heidelberg, 2002. Google Scholar
  19. Andrei Popescu and Dmitriy Traytel. Admissible types-to-pers relativization in higher-order logic. Proc. ACM Program. Lang., 7(POPL), January 2023. URL:
  20. Adrian Sampson. Probabilistic programming. Accessed: January 25. 2023.
  21. Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu. Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, bayesian inference, and optimization. Proceedings of the ACM on Programming Languages, 3(POPL):1-30, 2019. URL:
  22. Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani. Denotational validation of higher-order bayesian inference. Proc. ACM Program. Lang., 2(POPL), 2017. URL:
  23. Shashi Mohan Srivastava. A Course on Borel Sets. Springer, 1998. URL:
  24. Sam Staton. Commutative semantics for probabilistic programming. In Hongseok Yang, editor, Programming Languages and Systems, pages 855-879, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. Google Scholar
  25. Sam Staton. Probabilistic Programs as Measures, pages 43-74. Cambridge University Press, 2020. URL:
  26. Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha, Michael L. Wick, and Anindya Banerjee. Verification of ML systems via reparameterization, 2020. URL:
  27. Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. Proc. ACM Program. Lang., 3(POPL), January 2019. URL:
  28. Matthijs Vákár and Luke Ong. On s-finite measures and kernels, 2018. URL:
  29. Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. A new approach to probabilistic programming inference. In Proceedings of the 17th International conference on Artificial Intelligence and Statistics, pages 1024-1032, 2014. Google Scholar
  30. Hongseok Yang. Semantics of higher-order probabilistic programs with continuous distributions. Accessed: February 8. 2023.
  31. Yizhou Zhang and Nada Amin. Reasoning about “reasoning about reasoning”: Semantics and contextual equivalence for probabilistic programs with nested queries and recursion. Proc. ACM Program. Lang., 6(POPL), January 2022. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail