Document Open Access Logo

Evidence-Tracked Tape Semantics for Probabilistic Computation

Authors Liron Cohen , Tomer Samara

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.13.pdf
  • Filesize: 0.79 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
  • Theory of computation → Probabilistic computation
Keywords
  • probabilistic programming
  • random tapes
  • realizability
  • evidenced frames
  • program logic
  • monadic combinatory algebras

Metrics

Abstract

A standard intensional account of probabilistic computation represents a randomized program as a deterministic computation that consumes an explicit random tape. This yields a two-layer perspective: an intensional layer that makes reuse of randomness and correlation visible, and an extensional layer obtained by interpreting tapes under a chosen probability measure. We develop an evidence-tracked tape semantics using the monadic-core-to-evidenced-frame pipeline (and its induced realizability tripos), obtaining a higher-order logic in which entailments are witnessed by uniform evidence transformers. Quantitative statements are recovered by interpretation: once a tape measure is fixed, probabilities and expectations arise by extracting numerical summaries from tape-indexed predicates, and entailments yield sound inequalities, with an almost-sure quotient supporting probability-one reasoning. We also study intensional principles that are lost at the level of laws, including proof-relevant transport along realizable tape-rewiring maps and a canonical splitting discipline for stream tapes enforcing independent draws. Finally, we relate tape-based reasoning to an extensional law semantics via pushforward, isolating a probability-one must abstraction as a sound summary of tape-based proofs.

Cite As Get BibTex

Liron Cohen and Tomer Samara. Evidence-Tracked Tape Semantics for Probabilistic Computation. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.13

Author Details

Liron Cohen
  • Ben-Gurion University, Beer-Sheva, Israel
Tomer Samara
  • Ben-Gurion University, Beer-Sheva, Israel

Funding

This work was supported by Grant No. 2876/25 from the Israeli Science Foundation (ISF).

References

  1. Alejandro Aguirre and Shin-ya Katsumata. Weakest Preconditions in Fibrations. Electronic Notes in Theoretical Computer Science, 352:5-27, 2020. URL: https://doi.org/10.1016/j.entcs.2020.09.002.
  2. Robert J. Aumann. Borel Structures for Function Spaces. Illinois Journal of Mathematics, 5(4):614-630, December 1961. URL: https://doi.org/10.1215/ijm/1255631584.
  3. Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub. Relational Reasoning via Probabilistic Coupling, pages 387-401. Springer Berlin Heidelberg, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_27.
  4. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin. Probabilistic Relational Reasoning for Differential Privacy. ACM Transactions on Programming Languages and Systems, 35(3):1-49, November 2013. URL: https://doi.org/10.1145/2492061.
  5. Dan Boneh and Victor Shoup. A graduate course in applied cryptography, 2015. Google Scholar
  6. Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey. From Partial to Monadic: Combinatory Algebra with Effects. In Maribel Fernández, editor, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), volume 337 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1-14:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.14.
  7. Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey. Syntactic Effectful Realizability in Higher-Order Logic. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2025. URL: https://doi.org/10.1109/lics65433.2025.00009.
  8. Liron Cohen, Etienne Miquey, and Ross Tate. Evidenced Frames: A Unifying Framework Broadening Realizability Models. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, June 2021. URL: https://doi.org/10.1109/lics52264.2021.9470514.
  9. Ricardo Corin and Jerry den Hartog. A Probabilistic Hoare-Style Logic for Game-Based Cryptographic Proofs, pages 252-263. Springer Berlin Heidelberg, 2006. URL: https://doi.org/10.1007/11787006_22.
  10. Fredrik Dahlqvist, Alexandra Silva, and William Smith. Deterministic stream-sampling for probabilistic programming: semantics and verification . In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, Los Alamitos, CA, USA, June 2023. IEEE Computer Society. URL: https://doi.org/10.1109/LICS56636.2023.10175773.
  11. Fredrik Dahlqvist, Alexandra Silva, and William Smith. Deterministic Stream-Sampling for Probabilistic Programming: Semantics and Verification, June 2023. URL: https://doi.org/10.1109/lics56636.2023.10175773.
  12. 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, pages 1-14. ACM, July 2024. URL: https://doi.org/10.1145/3661814.3662126.
  13. Thomas Ehrhard. Differentials and Distances in Probabilistic Coherence Spaces. LIPIcs, Volume 131, FSCD 2019, 131:17:1-17:17, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.17.
  14. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Measurable Cones and Stable, Measurable Functions: a Model for Probabilistic Higher-Order Programming. Proceedings of the ACM on Programming Languages, 2(POPL):1-28, December 2017. URL: https://doi.org/10.1145/3158147.
  15. John T. Gill. Computational Complexity of Probabilistic Turing Machines. In Proceedings of the sixth annual ACM symposium on Theory of computing - STOC ’74, STOC ’74, pages 91-95. ACM Press, 1974. URL: https://doi.org/10.1145/800119.803889.
  16. Michèle Giry. A Categorical Approach to Probability Theory. In Categorical Aspects of Topology and Analysis, pages 68-85. Springer Berlin Heidelberg, 1982. URL: https://doi.org/10.1007/bfb0092872.
  17. Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. Probabilistic Programming. In Future of Software Engineering Proceedings, ICSE ’14, pages 167-181. ACM, May 2014. URL: https://doi.org/10.1145/2593882.2593900.
  18. 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. IEEE, June 2017. URL: https://doi.org/10.1109/lics.2017.8005137.
  19. J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts. Tripos Theory. Mathematical Proceedings of the Cambridge Philosophical Society, 88(2):205-232, September 1980. URL: https://doi.org/10.1017/s0305004100057534.
  20. Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs, pages 364-389. Springer Berlin Heidelberg, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_15.
  21. Dexter Kozen. Semantics of Probabilistic Programs. Journal of Computer and System Sciences, 22(3):328-350, June 1981. URL: https://doi.org/10.1016/0022-0000(81)90036-2.
  22. Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Springer Nature, United States, 2005. URL: https://doi.org/10.1007/b138392.
  23. Eugenio Moggi. Notions of Computation and Monads. Information and Computation, 93(1):55-92, July 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  24. Andrew M Pitts. Evaluation logic. In IV Higher Order Workshop, Banff 1990: Proceedings of the IV Higher Order Workshop, Banff, Alberta, Canada 10-14 September 1990, pages 162-189. Springer, 1991. URL: https://doi.org/10.1007/978-1-4471-3182-3_11.
  25. Andrew M. Pitts. Tripos Theory in Retrospect. Mathematical Structures in Computer Science, 12(3):265-279, June 2002. URL: https://doi.org/10.1017/s096012950200364x.
  26. Anish Saini, Athanasios Tsokanos, and Raimund Kirner. Quantum Randomness in Cryptography—A Survey of Cryptosystems, RNG-Based Ciphers, and QRNGs. Information, 13(8):358, July 2022. URL: https://doi.org/10.3390/info13080358.
  27. Sam Staton. Commutative semantics for probabilistic programming. In Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings, pages 855-879, Berlin, Heidelberg, 2017. Springer-Verlag. URL: https://doi.org/10.1007/978-3-662-54434-1_32.
  28. 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. ACM, July 2016. URL: https://doi.org/10.1145/2933575.2935313.
  29. John von Neumann. Various Techniques Used in Connection with Random Digits. In Notes by G. E. Forsythe, in National Bureau of Standards, Applied Mathematics Series, volume 12, pages 36-38. National Bureau of Standards, Washington, D. C., 1951. Google Scholar
  30. Noam Zilberstein, Derek Dreyer, and Alexandra Silva. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):522-550, April 2023. URL: https://doi.org/10.1145/3586045.
  31. Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti. A demonic Outcome Logic for Randomized Nondeterminism. Proceedings of the ACM on Programming Languages, 9(POPL):539-568, January 2025. URL: https://doi.org/10.1145/3704855.
  32. Noam Zilberstein, Alexandra Silva, and Joseph Tassarotti. Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants. Proc. ACM Program. Lang., 10(POPL), January 2026. URL: https://doi.org/10.1145/3776651.
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