Document Open Access Logo

A Convenient Fibration for Dependently-Typed Probability Theory

Authors Danel Ahman , Ohad Kammar , Rasmus Ejlers Møgelberg

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.4.pdf
  • Filesize: 0.92 MB
  • 27 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Denotational semantics
  • Theory of computation → Categorical semantics
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
  • Mathematics of computing → Nonparametric statistics
  • Mathematics of computing → Continuous mathematics
  • Software and its engineering → Data types and structures
  • Software and its engineering → Semantics
  • Software and its engineering → Domain specific languages
Keywords
  • probability theory
  • quasi-Borel space
  • Grothendieck fibration
  • fibred monad
  • conditional expectation
  • measure theory
  • random variables
  • dependent types
  • quasitopos
  • probabilistic programming
  • denotational semantics
  • synthetic measure theory

Metrics

Abstract

We describe semantic structures relevant for interpreting dependent types for statistical and probabilistic modelling. Our development extends the theory of quasi-Borel spaces (qbses) of Staton et. al, which support simply-typed, higher-order probability theory with continuous distributions. It is well-known that qbses can interpret a dependent-type theory supporting dependent function-spaces through the codomain fibration. We define an equivalent split fibration based on the family fibration, which we call quasi-Borel families (qbfs), characterise its structure, equip it with fibred monads of measures and probability, and use them to develop dependently-typed probability theory.
We characterise the structure of the qbf fibration that is relevant for dependently-typed probability theory in elementary form. Our characterisations include: context extension, dependent pairs, dependent functions, extensional identity types, fibred products and coproducts, subspaces, a universe of propositions, and straightforward internalisation and externalisation principles for discrete spaces. We use these concepts to define fibred distribution and probability monads, the semantic structure needed to interpret probability distributions under a dependent context. We show that this structure satisfies a fibred version of Kock’s synthetic measure theory. We also use these concepts to develop a qbs counterpart to Kolmogorov’s conditional expectation. Our main result is a version of the conditional expectation that, under standard regularity assumptions, is measurable in both the random variables we are conditioning, and the observation map we are conditioning by.

Cite As Get BibTex

Danel Ahman, Ohad Kammar, and Rasmus Ejlers Møgelberg. A Convenient Fibration for Dependently-Typed Probability Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 4:1-4:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.4

Author Details

Danel Ahman
  • Institute of Computer Science, University of Tartu, Estonia
Ohad Kammar
  • LFCS, School of Informatics, University of Edinburgh, UK
Rasmus Ejlers Møgelberg
  • IT University of Copenhagen, Denmark

Funding

  • Ahman, Danel: supported by the Estonian Research Council grant PRG2764.
  • Kammar, Ohad: supported by an ARIA SGAI TA1.1 grant and a Royal Society URF award.
  • Møgelberg, Rasmus Ejlers: supported by the Independent Research Fund Denmark, grant 2032-00134B

Acknowledgements

We thank the chairs and the anonymous referees, and these people for interesting and useful discussions and suggestions: Jonas Dickhöfer, Sergey Goncharov, Chris Heunen, Paul Blain Levy, Justus Matthiesen, Sean K. Moss, Matija Pretnar, Adam Ścibior, Jesse Aaron Sigal, Alex K. Simpson, Sam Staton, Matthijs Vákár, Théo Chengkai Wang, Hongseok Yang, and the participants of the following meetings: CIRM Logic of Probabistic Programming (Logic and Interactions'22), Scottish Programming Language and Verification Summer School '22, Australian National University Logic Summer School '23, POPL'24 TutorialFest, Laboratory for Software Science Tartu Supernumerary Course '25, and Aarhus University Logic and Semantics Seminar '26.

References

  1. Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang., 5(POPL), 2021. URL: https://doi.org/10.1145/3434320.
  2. Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht. A calculus for amortized expected runtimes. Proc. ACM Program. Lang., 7(POPL):1957-1986, 2023. URL: https://doi.org/10.1145/3571260.
  3. Martin E. Bidlingmaier, Florian Faissole, and Bas Spitters. Synthetic topology in homotopy type theory for probabilistic programming. Mathematical Structures in Computer Science, 31(10):1301-1329, 2021. URL: https://doi.org/10.1017/S0960129521000165.
  4. Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, and Lars Birkedal. Guarded dependent type theory with coinductive types. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures, pages 20-35, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. Google Scholar
  5. Linan Chen, Florence Clerc, and Prakash Panangaden. Behavioural equivalences for continuous-time markov processes. Math. Struct. Comput. Sci., 33(4-5):222-258, 2023. URL: https://doi.org/10.1017/S0960129523000099.
  6. Linan Chen, Florence Clerc, and Prakash Panangaden. A behavioural pseudometric for continuous-time markov processes. In Parosh Aziz Abdulla and Delia Kesner, editors, Foundations of Software Science and Computation Structures - 28th International Conference, FoSSaCS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, volume 15691 of Lecture Notes in Computer Science, pages 24-44. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90897-2_2.
  7. Donald L Cohn. Measure theory. Birkhäuser Advanced Texts Basler Lehrbücher. Birkhauser Boston, Secaucus, NJ, 2 edition, July 2013. Google Scholar
  8. Thierry Coquand and Bas Spitters. Integrals and valuations. J. Log. Anal., 1, 2009. URL: http://logicandanalysis.org/index.php/jla/article/view/14/12.
  9. Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton. Affine monads and lazy structures for bayesian programming. Proc. ACM Program. Lang., 7(POPL):1338-1368, 2023. URL: https://doi.org/10.1145/3571239.
  10. Pietro Di Gianantonio and Abbas Edalat. A cartesian closed category for random variables. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3661814.3662126.
  11. Henry Ford and Samuel Crowther. My life and work. William Heinemann Ltd., 1922. Google Scholar
  12. Pietro Di Gianantonio and Abbas Edalat. A domain-theoretic framework for conditional probability and bayesian updating in programming, 2025. URL: https://doi.org/10.48550/arXiv.2502.00949.
  13. Jean Goubault-Larrecq and Daniele Varacca. Continuous random variables. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pages 97-106, 2011. URL: https://doi.org/10.1109/LICS.2011.23.
  14. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory . In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, Los Alamitos, CA, USA, June 2017. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2017.8005137.
  15. Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, pages 427-441, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  16. Aumann Robert J. Borel structures for function spaces. Illinois Journal of Mathematics, 5:614-630, 1961. Google Scholar
  17. Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. Google Scholar
  18. Bart Jacobs. Urns & tubes. Compositionality, 4:4, 2022. URL: https://doi.org/10.32408/COMPOSITIONALITY-4-4.
  19. Peter T Johnstone. Sketches of an Elephant A Topos Theory Compendium. Oxford University Press, Oxford, England, September 2002. URL: https://doi.org/10.1093/oso/9780198515982.001.0001.
  20. Olav Kallenberg. Foundations of modern probability. Probability Theory and Stochastic Modelling. Springer Nature, Cham, Switzerland, 3 edition, February 2021. Google Scholar
  21. Ohad Kammar. Simply-typed measurability, 2024. Unpublished preprint. Google Scholar
  22. Anders Kock. Commutative monads as a theory of distributions. Theory and Applications of Categories, 26(4):97-131, 2012. Google Scholar
  23. Dexter Kozen. Kolmogorov extension, martingale convergence, and compositionality of processes. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 692-699, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2933610.
  24. John M. Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, and Steven Holtzen. A nominal approach to probabilistic separation logic. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3661814.3662135.
  25. Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, and Lars Birkedal. Modular specifications and implementations of random samplers in higher-order separation logic. In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP '26, pages 368-382, New York, NY, USA, 2026. Association for Computing Machinery. URL: https://doi.org/10.1145/3779031.3779109.
  26. Conor McBride. Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh, UK, 2000. URL: https://hdl.handle.net/1842/374.
  27. Eigil Fjeldgren Rischel. Markov Fibrations. PhD thesis, University of Strathclyde, 2026. http://purl.org/coar/resource_type/c_db06. Google Scholar
  28. Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman. Probabilistic programming semantics for name generation. Proc. ACM Program. Lang., 5(POPL), 2021. URL: https://doi.org/10.1145/3434292.
  29. 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), December 2017. URL: https://doi.org/10.1145/3158148.
  30. Alex Simpson. Probability Sheaves and the Giry Monad. In Filippo Bonchi and Barbara König, editors, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017), volume 72 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1:1-1:6, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CALCO.2017.1.
  31. Alex Simpson. Equivalence and conditional independence in atomic sheaf logic. In Proceedings of the Thirty ninth Annual IEEE Symposium on Logic in Computer Science (LICS 2024), pages 70:1-70:14. IEEE Computer Society Press, July 2024. URL: https://doi.org/10.1145/3661814.3662132.
  32. William Smith. Sampling languages: Semantics and verification of sampling-based inference algorithms for probabilistic programming. PhD thesis, University of Strathclyde, 2013. https://adam.gundry.co.uk/pub/thesis/. Google Scholar
  33. Toby St Clere Smithe. Copy-composition for probabilistic graphical models. In Michael Johnson and David Jaz Myers, editors, Proceedings Seventh International Conference on Applied Category Theory 2024, Oxford, United Kingdom, 17 - 21 June 2024, volume 429 of Electronic Proceedings in Theoretical Computer Science, pages 146-173. Open Publishing Association, 2025. URL: https://arxiv.org/abs/2406.08286v1.
  34. Toby St Clere Smithe. Copy-composition for probabilistic graphical models. Electronic Proceedings in Theoretical Computer Science, 429:146-173, September 2025. revised (version 2). URL: https://doi.org/10.4204/eptcs.429.8.
  35. Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Annebet Zwart, Alejandro Aguirre, and Lars Birkedal. Modelling recursion and probabilistic choice in guarded type theory. Proc. ACM Program. Lang., 9(POPL), 2025. URL: https://doi.org/10.1145/3704884.
  36. Sam Staton. Commutative semantics for probabilistic programming. In Hongseok Yang, editor, Programming Languages and Systems, pages 855-879, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-54434-1_32.
  37. Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 525-534, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2935313.
  38. Norman Earl Steenrod. A convenient category of topological spaces. Michigan Mathematical Journal, 14(2):133-152, 1967. URL: https://doi.org/10.1307/mmj/1028999711.
  39. Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. Proc. ACM Program. Lang., 3(POPL), 2019. URL: https://doi.org/10.1145/3290349.
  40. Matthijs Vákár and Luke Ong. On s-finite measures and kernels, 2018. URL: https://arxiv.org/abs/1810.01837.
  41. David Williams. Probability with Martingales. Cambridge Mathematical Textbooks. Cambridge University Press, Cambridge, England, 1991. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact