pith. sign in

arxiv: 2511.10135 · v4 · submitted 2025-11-13 · 💻 cs.LO · cs.PL

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)

Kwing Hei Li , Alejandro Aguirre , Joseph Tassarotti , Lars Birkedal This is my paper

Pith reviewed 2026-05-17 22:24 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords separation logiccontextual refinementprobabilistic programsconcurrent programshigher-order stateIrisRocq
0
0 comments X p. Extension

The pith

Foxtrot is the first higher-order separation logic for proving contextual refinement of concurrent probabilistic programs with local state.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Foxtrot as a separation logic for establishing that one higher-order concurrent probabilistic program contextually refines another. A reader would care because these programs arise in randomized algorithms and cryptography, where threads interact through shared state and draw from complex probability distributions. Foxtrot reuses standard concurrent separation logic tools such as invariants and ghost resources while adding probabilistic devices like tape presampling and error-amplification induction. The authors show the logic works on examples that range from adversarial coin flips to a uniform random bytes function in a real cryptographic library, with every result checked inside the Rocq proof assistant.

Core claim

Foxtrot is the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning principles from standard concurrent separation logic, e.g. invariants and ghost resources, and supports advanced probabilistic reasoning principles for reasoning about complex probability distributions induced by concurrent threads, e.g. tape presampling and induction by error amplification.

What carries the argument

Foxtrot logic, an extension of the Iris separation logic that integrates concurrency invariants with probabilistic tape and error-amplification rules while remaining sound.

If this is right

  • Contextual refinement can now be proved for programs that interleave higher-order functions, shared local state, concurrency, and arbitrary probability distributions.
  • Adversarial coin-flip protocols and uniform random generation routines from cryptographic libraries become verifiable targets.
  • The same logic supplies both invariant-based concurrency reasoning and distribution-sensitive probabilistic reasoning in a single framework.
  • All claims, including soundness, have been machine-checked in Rocq using the Iris library.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same machinery may scale to probabilistic distributed systems whose threads communicate over networks rather than shared memory.
  • The reliance on an internal axiom of choice raises the question whether weaker choice principles suffice for other effect combinations such as nondeterminism plus probability.
  • Mechanized libraries built on Foxtrot could serve as a foundation for verifying larger randomized data structures and protocols.

Load-bearing premise

Soundness of the logic depends on a version of the axiom of choice inside the Iris framework.

What would settle it

A concrete pair of programs that are contextually equivalent yet cannot be proved equivalent inside Foxtrot, or a pair that is not equivalent yet the logic derives a refinement proof, would show the central claim is false.

Figures

Figures reproduced from arXiv: 2511.10135 by Alejandro Aguirre, Joseph Tassarotti, Kwing Hei Li, Lars Birkedal.

Figure 1
Figure 1. Figure 1: Systems for proving contextual refinement (Logic = implemented as a logic, ND = only nondeterminism). [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Entropy mixer example. We summarize this subsection with the following slogan: Slogan 1: Invariants, ghost resources, and ht-couple are (almost) all you need. 3.3 Advanced Rules Previously, we saw the standard coupling rule ht-couple for coupling a rand 𝑁 on the left with one on the right under a bijective function. However, unsurprisingly, there are times where it is not the case that there is convenientl… view at source ↗
Figure 3
Figure 3. Figure 3: Batch-sampling example. Let us first consider the left-to-right refinement first. To reason about random samplings occurring in different threads in batchImpl, Foxtrot uses presampling tapes (first introduced in Clutch [18]) to “compress” multiple samplings and reason about them as if they are one. 𝑣 ∈Val ::= . . . | 𝜅 ∈ Label 𝑒 ∈ Expr ::= . . . | tape 𝑒 | rand𝑒1 𝑒2 𝜎 ∈ State ≜ (Loc fin −⇀Val) × (Label fin… view at source ↗
Figure 4
Figure 4. Figure 4: Rejection sampler example. Here, we sadly cannot use the trick presented in Slogan 2; instead of trying to relate two rands with one, we are trying to relate a pair of rands in a somewhat unnatural manner. If the rejection sampler samples a value ≤ 𝑀, we want that value to be coupled with rand 𝑀. Otherwise if we sampled a value > 𝑀, we do not want to step rand 𝑀 at all. In other words, we only want to perf… view at source ↗
Figure 5
Figure 5. Figure 5: Adversarial von Neumann coin example. Both programs in [PITH_FULL_IMAGE:figures/full_fig_p014_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Sodium randombytes_uniform implementation. [PITH_FULL_IMAGE:figures/full_fig_p015_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Inductive Definition of the Spec Step Precondition sstep [PITH_FULL_IMAGE:figures/full_fig_p018_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: The nondet and diverge programs. The program nondet is a function that first creates a reference containing 0. It then spawns a thread that repeatedly increments the reference, and the main thread reads from the reference and returns the value. It is trivial to see that for any natural number 𝑛, there exists some scheduling such that nondet () returns 𝑛, as captured by the rule ht-nondet. In fact, if this … view at source ↗
Figure 9
Figure 9. Figure 9: Example without optimal scheduling. What is the least upper bound of the termination probability of both programs? It is obviously 1 for the right-hand side program, and it turns out it is also 1 for the left-hand side program as well, even though it never terminates with probability 1 for any scheduling! This is because for any natural number 𝑛, we can find some scheduling such that the left-hand side pro… view at source ↗
Figure 10
Figure 10. Figure 10: One-time pad example. Unsurprisingly, the right-to-left direction is not too difficult. Since otpImpl resides on the right￾hand side of the refinement, we can take advantage of the angelic nondeterminism of the specifica￾tion program and choose the interleaving that first resolves the first thread of otpImpl followed by the second. For the sampling of the second thread, we couple it with the one in otpSpe… view at source ↗
Figure 11
Figure 11. Figure 11: Equational theory. Here, 𝜏 ∈ Type and ∀𝑖 ∈ {1, 2, 3}. ∅ ⊢ 𝑒𝑖 : 𝜏. The last equation is the distributive law of a convex semilattice. Currently, Foxtrot is only expressive enough to prove one direction of the equivalence. We hypothesis that the other direction requires more advanced logical facilities for reasoning about probability and nondeterminism such as prophecy variables [1, 2, 22] (as it is the cas… view at source ↗
read the original abstract

We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning principles from standard concurrent separation logic, e.g. invariants and ghost resources, and supports advanced probabilistic reasoning principles for reasoning about complex probability distributions induced by concurrent threads, e.g. tape presampling and induction by error amplification. The integration of these strong reasoning principles is highly non-trivial due to the combination of probability and concurrency in the language and the complexity of the Foxtrot model; the soundness of the logic relies on a version of the axiom of choice within the Iris logic, which is not used in earlier work on Iris-based logics. We demonstrate the expressiveness of Foxtrot on a wide range of examples, including the adversarial von Neumann coin and the $\mathsf{randombytes\_uniform}$ function of the Sodium cryptography software library. All results have been mechanized in the Rocq proof assistant and the Iris separation logic framework.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper presents Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. It inherits concurrency reasoning principles such as invariants and ghost resources from standard concurrent separation logic and supports probabilistic reasoning principles including tape presampling and induction by error amplification. The soundness of the logic is established within the Iris framework and the entire development has been mechanized in Rocq, though it relies on a version of the axiom of choice inside Iris that is not used in prior Iris-based logics. The logic is demonstrated on examples including the adversarial von Neumann coin and the randombytes_uniform function from the Sodium cryptography library.

Significance. If the central claims hold, this constitutes a significant advance by enabling formal reasoning about contextual refinement in a setting that combines higher-order features, concurrency, and probability with local state. The mechanization in Rocq and Iris provides strong, reproducible evidence for the soundness of the logic and the validity of the example proofs, which is a notable strength. The practical examples further indicate potential utility for verifying real probabilistic concurrent code.

major comments (1)
  1. [Soundness] The soundness theorem relies on a version of the axiom of choice within the Iris logic. This step is disclosed in the abstract and introduction but is not used in earlier Iris-based logics; the mechanized development should isolate this axiom application (e.g., in the model construction or adequacy proof) and provide explicit verification or justification that it preserves the independence of the grounding.
minor comments (2)
  1. [Abstract] The abstract is concise but could mention the mechanization platform (Rocq/Iris) in the opening sentence to foreground the reproducibility of the results.
  2. [Introduction] Notation for higher-order local state and tape presampling could be introduced with a small illustrative example in the introduction to improve accessibility for readers new to the combination of features.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful review and constructive suggestion. We address the single major comment below and will update the mechanized development and paper accordingly.

read point-by-point responses

  1. Referee: [Soundness] The soundness theorem relies on a version of the axiom of choice within the Iris logic. This step is disclosed in the abstract and introduction but is not used in earlier Iris-based logics; the mechanized development should isolate this axiom application (e.g., in the model construction or adequacy proof) and provide explicit verification or justification that it preserves the independence of the grounding.

    Authors: We appreciate the referee drawing attention to the use of the axiom of choice. As already stated in the abstract and introduction, this axiom is required for the soundness of Foxtrot but was not needed in prior Iris-based logics. We agree that isolating its application will improve clarity. In the revised development we will extract the axiom usage into a dedicated, clearly marked lemma inside the model construction (separate from the main adequacy proof) and add code comments plus a short paragraph in the paper explaining that the axiom is invoked only to select representatives for the probabilistic model and does not affect the independence of the grounding or the validity of the separation-logic rules. This change is feasible within the existing Rocq/Iris infrastructure. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper defines Foxtrot as a new higher-order separation logic inside the established Iris framework and supplies a complete mechanized soundness proof in Rocq. All reasoning principles (invariants, ghost resources, tape presampling, error-amplification induction) are derived from the Iris model rather than from any self-referential definition or fitted parameter. The explicit disclosure that soundness uses a version of the axiom of choice inside Iris (absent from prior Iris logics) is an external assumption, not a circular reduction. Because the entire development is machine-checked against an independently verified base logic, the derivation chain remains self-contained and does not reduce to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the soundness of Foxtrot inside Iris, which invokes an axiom of choice not used in earlier Iris logics; no free parameters or new entities are introduced beyond the logic rules themselves.

axioms (1)
  • ad hoc to paper A version of the axiom of choice within the Iris logic
    Explicitly required for soundness as stated in the abstract; not used in prior Iris-based logics.

pith-pipeline@v0.9.0 · 5485 in / 1174 out tokens · 29580 ms · 2026-05-17T22:24:22.712965+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

44 extracted references · 44 canonical work pages

  1. [1]

    Abadi and L

    M. Abadi and L. Lamport. 1988. The existence of refinement mappings. In [1988] Proceedings. Third Annual Symposium on Logic in Computer Science . 165–175. doi:10.1109/LICS.1988.5115

    work page doi:10.1109/lics.1988.5115 1988

  2. [2]

    Martín Abadi and Leslie Lamport. 1991. The existence of refinement mappings. Theoretical Computer Science 82, 2 (1991), 253–284. doi:10.1016/0304-3975(91)90224-P

    work page doi:10.1016/0304-3975(91)90224-p 1991

  3. [3]

    Alejandro Aguirre and Lars Birkedal. 2023. Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. Proceedings of the ACM on Programming Languages 7 (9 Jan. 2023), 33–60. doi:10.1145/3571195 Publisher Copyright: © 2023 Owner/Author

    work page doi:10.1145/3571195 2023

  4. [4]

    and de Medeiros, Markus and Li, Kwing Hei and Gregersen, Simon Oddershede and Tassarotti, Joseph and Birkedal, Lars , title =

    Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal. 2024. Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. Proc. ACM Program. Lang. 8, ICFP, Article 246 (Aug. 2024), 33 pages. doi:10.1145/3674635

    work page doi:10.1145/3674635 2024

  5. [5]

    James Aspnes and Eric Ruppert. 2016. Depth of a Random Binary Search Tree with Concurrent Insertions. InDistributed Computing, Cyril Gavoille and David Ilcinkas (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 371–384

    work page 2016

  6. [6]

    Lars Birkedal, Aleš Bizjak, and Jan Schwinghammer. 2013. Step-Indexed Relational Reasoning for Countable Nonde- terminism. Logical Methods in Computer Science Volume 9, Issue 4 (Oct. 2013). doi:10.2168/lmcs-9(4:4)2013

    work page doi:10.2168/lmcs-9(4:4)2013 2013

  7. [7]

    Aleš Bizjak and Lars Birkedal. 2015. Step-Indexed Logical Relations for Probability. In Foundations of Software Science and Computation Structures, Andrew Pitts (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 279–294

    work page 2015

  8. [8]

    Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. 2013. Coquelicot: A User-Friendly Library of Real Analysis for Coq. (Sept. 2013). https://inria.hal.science/hal-00860648 working paper or preprint

    work page 2013

  9. [9]

    Raphaëlle Crubillé and Ugo Dal Lago. 2014. On Probabilistic Applicative Bisimulation and Call-by-Value 𝜆-Calculi. In Programming Languages and Systems , Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 209–228

    work page 2014

  10. [10]

    Ryan Culpepper and Andrew Cobb. 2017. Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring. In Programming Languages and Systems , Hongseok Yang (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 368–392

    work page 2017

  11. [11]

    Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. 2014. On coinductive equivalences for higher-order probabilistic functional programs. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, California, USA) (POPL ’14). Association for Computing Machinery, New York, NY, USA, 297–308. doi:10.1145/25358...

    work page doi:10.1145/2535838.2535872 2014

  12. [12]

    Frank Denis. 2013. The Sodium cryptography library. https://download.libsodium.org/doc/ 22 K. H. Li, A. Aguirre, J. Tassarotti, and L. Birkedal

    work page 2013

  13. [13]

    Radu Diaconescu. 1975. Axiom of Choice and Complementation. Proc. Amer. Math. Soc. 51, 1 (1975), 176–178. http://www.jstor.org/stable/2039868

    work page arXiv 1975

  14. [14]

    Thomas Ehrhard, Christine Tasson, and Michele Pagani. 2014. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, California, USA) (POPL ’14). Association for Computing Machinery, New York, NY, USA, 309–320. doi:10.1145/2535838.2535865

    work page doi:10.1145/2535838.2535865 2014

  15. [15]

    David Evans, Vladimir Kolesnikov, and Mike Rosulek. 2018. . doi:10.1561/3300000019

    work page doi:10.1561/3300000019 2018

  16. [16]

    Ira Fesefeldt, Joost-Pieter Katoen, and Thomas Noll. 2022. Towards Concurrent Quantitative Separation Logic. In 33rd International Conference on Concurrency Theory (CONCUR 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 243), Bartek Klin, Sławomir Lasota, and Anca Muscholl (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, D...

    work page doi:10.4230/lipics.concur.2022.25 2022

  17. [17]

    Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2021. ReLoC Reloaded: A Mechanized Relational Logic for Fine- Grained Concurrency and Logical Atomicity. Log. Methods Comput. Sci. 17, 3 (2021). doi:10.46298/LMCS-17(3:9)2021

    work page doi:10.46298/lmcs-17(3:9)2021 2021

  18. [18]

    Haselwarter and Joseph Tassarotti and Lars Birkedal , title =

    Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. 2024. Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proc. ACM Program. Lang. 8, POPL, Article 26 (Jan. 2024), 32 pages. doi:10.1145/3632868

    work page doi:10.1145/3632868 2024

  19. [19]

    Haselwarter and Kwing Hei Li and Alejandro Aguirre and Simon Oddershede Gregersen and Joseph Tassarotti and Lars Birkedal , title =

    Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal. 2025. Approximate Relational Reasoning for Higher-Order Probabilistic Programs. Proc. ACM Program. Lang. 9, POPL, Article 41 (Jan. 2025), 31 pages. doi:10.1145/3704877

    work page doi:10.1145/3704877 2025

  20. [20]

    Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 . 256–269. doi:10.1145/2951913.2951943

    work page doi:10.1145/2951913.2951943 2016

  21. [21]

    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20. doi:10.1017/S0956796818000151

    work page doi:10.1017/s0956796818000151 2018

  22. [22]

    Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs

    work page

  23. [23]

    The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang. 4, POPL, Article 45 (Dec. 2019), 32 pages. doi:10.1145/3371113

    work page doi:10.1145/3371113 2019

  24. [24]

    Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015 . 637–650. doi:10...

    work page doi:10.1145/2676726.2676980 2015

  25. [25]

    Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. 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, Sw...

    work page doi:10.1007/978-3-662-54434-1_26 2017

  26. [26]

    Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 205–217. doi:10.1145/3009837.3009855

    work page doi:10.1145/3009837.3009855 2017

  27. [27]

    and Tassarotti, Joseph and Birkedal, Lars , title =

    Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. 2025. Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs. Proc. ACM Program. Lang. 9, ICFP, Article 245 (Aug. 2025), 30 pages. doi:10.1145/3747514

    work page doi:10.1145/3747514 2025

  28. [28]

    Lindvall

    T. Lindvall. 2002. Lectures on the Coupling Method . Dover Publications, Incorporated

    work page 2002

  29. [29]

    Janine Lohse and Deepak Garg. 2024. An Iris for Expected Cost Analysis. arXiv:2406.00884 [cs.PL]

    work page arXiv 2024

  30. [30]

    Annabelle McIver, Tahiry Rabehaja, and Georg Struth. 2016. Probabilistic rely-guarantee calculus.Theoretical Computer Science 655 (2016), 120–134. doi:10.1016/j.tcs.2016.01.016 Quantitative Aspects of Programming Languages and Systems (2013-14)

    work page doi:10.1016/j.tcs.2016.01.016 2016

  31. [31]

    Robert Morris. 1978. Counting large numbers of events in small registers. Commun. ACM 21, 10 (Oct. 1978), 840–842. doi:10.1145/359619.359627

    work page doi:10.1145/359619.359627 1978

  32. [32]

    David Sabel, Manfred Schmidt-Schauß, and Luca Maio. 2022. Contextual Equivalence in a Probabilistic Call-by- Need Lambda-Calculus. In Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming (Tbilisi, Georgia) (PPDP ’22). Association for Computing Machinery, New York, NY, USA, Article 4, 15 pages. doi:10.1145/3...

    work page doi:10.1145/3551357.3551374 2022

  33. [33]

    Tetsuya Sato. 2016. Approximate Relational Hoare Logic for Continuous Random Samplings. In The Thirty-second Conference on the Mathematical Foundations of Programming Semantics, MFPS 2016 . doi:10.1016/J.ENTCS.2016.09.043

    work page doi:10.1016/j.entcs.2016.09.043 2016

  34. [34]

    Joseph Tassarotti and Robert Harper. 2019. A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3, POPL, Article 64 (Jan. 2019), 30 pages. doi:10.1145/3290377 Contextual Refinement of Higher-Order Concurrent Probabilistic Programs 23

    work page doi:10.1145/3290377 2019

  35. [35]

    The Rocq Development Team. 2024. The Rocq Prover. doi:10.5281/zenodo.11551307

    work page doi:10.5281/zenodo.11551307 2024

  36. [36]

    Hermann Thorisson. 2000. Coupling, stationarity, and regeneration. Springer-Verlag, New York. xiv+517 pages

    work page 2000

  37. [37]

    A. Timany. 2018.Contributions in Programming Languages Theory: Logical Relations and Type Theory. Ph. D. Dissertation. , Faculty of Engineering Science, Science, Engineering and Technology Group. https://lirias.kuleuven.be/1838165 Jacobs, B. (supervisor), Piessens, F. (cosupervisor)

    work page arXiv 2018

  38. [38]

    Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2024. A Logical Approach to Type Soundness. J. ACM 71, 6 (2024), 40:1–75

    work page 2024

  39. [39]

    Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer

    Aaron J. Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome, Italy) (POPL ’13). Association for Computing Machinery, New York, NY, USA, 343–356. doi:10.1145/2429069.2429111

    work page doi:10.1145/2429069.2429111 2013

  40. [40]

    Daniele Varacca and Glynn Winskel. 2006. Distributing probability over non-determinism. Mathematical. Structures in Comp. Sci. 16, 1 (Feb. 2006), 87–113. doi:10.1017/S0960129505005074

    work page doi:10.1017/s0960129505005074 2006

  41. [41]

    John von Neumann. 1961. John von Neumann Collected Works . Vol. 5: Design of Computers, Theory of Automata and Numerical Analysis. Pergamon Press, Oxford, England, Chapter Various Techniques Used in Connection with Random Digits, 768–770. Notes by George E. Forsythe and reproduced from J. Res. Nat. Bus. Stand. Appl. Math. Series, vol. 3, pp. 36–38 (1955)

    work page 1961

  42. [42]

    Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, and Andrew Cobb. 2018. Contextual equivalence for a probabilistic language with continuous random variables and recursion. Proc. ACM Program. Lang. 2, ICFP, Article 87 (July 2018), 30 pages. doi:10.1145/3236782

    work page doi:10.1145/3236782 2018

  43. [43]

    Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proc. ACM Program. Lang. 7, OOPSLA1, Article 93 (April 2023), 29 pages. doi:10.1145/3586045

    work page doi:10.1145/3586045 2023

  44. [44]

    information-theoretically secure

    Noam Zilberstein, Alexandra Silva, and Joseph Tassarotti. 2024. Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants. arXiv:2411.11662 [cs.LO] https://arxiv.org/abs/2411.11662 24 K. H. Li, A. Aguirre, J. Tassarotti, and L. Birkedal A Auxiliary Programs We introduce two auxiliary programs (Figure 8): nondet and di...

    work page arXiv 2024