Pith. sign in

REVIEW 3 major objections 4 minor 43 references

Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary

T0 review · 3 major / 4 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read opOL is a proof system whose derivable triples are valid for every oblivious-adversary schedule, with frame preservation and zero nontermination probability.

desk verdict A substantial, well-engineered program logic for fixed-tape oblivious schedulers, but the advertised threat model is broader than the formal model unless the observation interface is pinned down. read the letter →

arxiv 2607.16533 v1 pith:A63F7BA7 submitted 2026-07-17 cs.PL cs.LO

Hanxi Chen , Noam Zilberstein , Andrew C. Myers , Alexandra Silva This is my paper · ORCID
classification cs.PLcs.LO MSC 68Q6003B70
keywords probabilisticprogramlogicobliviousadversaryseparationindependenceschedulerconsumptionalmost-sureterminationrandomizedalgorithmstotalcorrectness
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper aims to make correctness proofs for randomized programs with an oblivious adversary compositional. Its central claim is a soundness theorem: any triple derived in opOL is valid against every fixed schedule, preserves framed resources, and implies almost-sure termination. The key move is to model the adversary as an infinite tape of choices and to track how many tape entries each branch consumes; a random outcome is private exactly when it is independent of that count. This lets the logic keep a frame rule for nondeterministic choice, which prior adaptive-adversary logics could not. The paper tests the logic on paging, leader election, and Monty Hall, where the obliviousness assumption is essential.

What carries the argument

The oblivious monad O(X)=Sched→N→D⊥(X×N), a probability monad layered over a reader for the immutable schedule and a state for the current index. The count of consumed tape entries is the only channel by which control flow can leak random outcomes to the fixed schedule; assertions are resources over probability spaces with memory and count observations, and the priv/leak modes attach to probabilistic outcome conjunctions. The Frame rule and ND rule are sound precisely because stability and privacy conditions control this count channel.

What would settle it

Construct a program whose random branch and schedule count are independent, but where an adversary with a fixed tape can still correlate its later choice with the random draw through an observable not represented in the denotation, such as execution time or memory access pattern; in opOL's model such a leak is invisible, so a derivable triple could fail against that stronger adversary.

Watch

Extended reading notes

Core claim

The central claim is that obliviousness can be made compositional by encoding schedule consumption as a resource. The denotation O(X)=Sched→N→D⊥(X×N) represents a program as a function from a fixed schedule and current index to a distribution over outputs and updated indices. Random branches that consume different numbers of schedule entries can leak entropy to the adversary; assertions carry a priv/leak mode that records whether a sampled variable is independent of the count. Soundness shows every derivable triple holds for all schedules and, since validity quantifies over resources without nontermination, implies total correctness. The logic recovers adaptive reasoning as a special case an

Load-bearing premise

The guarantees rest on the modeling premise that an oblivious adversary's only power is a fixed tape of choices read in order, so that a random outcome is hidden exactly when it is independent of the tape position; if the real adversary could observe timing or partial outputs, the logic's compositionality would not transfer.

Editorial extensions

If this is right

  • Every derivable opOL triple is valid for all schedules: postconditions hold, frames are preserved, and nontermination probability is zero.
  • Adaptive-adversary proof rules remain sound in the oblivious model because the oblivious semantics is a refinement of the adaptive powerdomain semantics.
  • Private random sources can be framed across later nondeterministic choices, so independence facts survive globally rather than being destroyed by each adversarial step.
  • The Bounded-Rank rule yields almost-sure termination proofs by giving a uniformly positive probability of rank decrease per block of iterations.
  • Case studies on paging, leader election, and Monty Hall show the logic can express guarantees that adaptive logics cannot.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the tape-index channel is the only leakage, the logic's guarantees suggest a quantitative measure: the probability that the adversary can guess a random source is governed by the marginal of the count conditioned on that source.
  • The model is a template for other resource-aware logics: any observable consumption channel, such as time or memory access pattern, could be wrapped as a resource and tracked with the same independence discipline.
  • The paging proof could plausibly be extended from bounds on the probability of many misses to expected competitive ratios, since the invariant already bounds the miss distribution.
  • Concurrency is the stated next step; the tape model assumes adversarial choices occur only at explicit nondeterministic commands, so the resource bookkeeping would need extension if scheduling occurs at every interleaving step.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper introduces Oblivious Probabilistic Outcome Logic (opOL), a Hoare-style logic for probabilistic programs whose nondeterminism is resolved by an oblivious adversary modeled as a fixed infinite schedule tape. The semantics is built on monad O(X) = Sched -> N -> D⊥(X×N), which records both the output memory and the number of schedule entries consumed. The logic tracks schedule consumption as a resource, distinguishes private from leaky random sources through probabilistic independence, and provides compositional rules including a restricted Frame rule, rules for nondeterministic choice, and a bounded-rank rule for almost-sure termination. The main metatheorem (Theorem 5.2) asserts soundness of all derivable triples with respect to this denotational model. The paper also sketches three case studies—Monty Hall, leader election, and randomized paging—and claims that the metatheory and case studies are mechanized in Lean 4.

Significance. If the results hold, opOL is a substantial advance over adaptive-adversary logics such as dOL and pcOL: it recovers a sound Frame rule for nondeterministic choice under an oblivious adversary and gives compositional, total-correctness-style reasoning for programs that are outside the reach of adaptive models. The paper's core contribution is carefully stated: the resource-based tracking of schedule consumption, the private/leaky distinction, and the direct soundness proofs against a denotational semantics are presented in detail in the appendices. The three case studies are nontrivial and provide concrete evidence of expressiveness. The claimed Lean mechanization, if accompanied by a verifiable artifact, would be a further significant strength; as submitted, that claim cannot yet be checked.

major comments (3)
  1. [Sections 2.1, 3.2, Definition 5.1] The paper equates 'oblivious adversary' with a fixed schedule tape whose only observable is the tape index n. The informal threat model ('does not see the outcomes of random draws') is broader: an adversary that could observe elapsed iterations, as in C = (x:≈Ber(1/2); z:=x; while x=1 do x:=0; y←[0,1]), would learn x even though bits(while)={0} makes z private in O. The soundness theorem is relative to the fixed-tape model, so this is not an internal inconsistency; however, the advertised scope is load-bearing for the Frame, ND, NAssign, and priv/leak rules. Please either formalize the adversary's observation interface and prove equivalence, or explicitly state that the logic is scoped to the fixed-tape model and that other side-channel observables are out of scope.
  2. [Abstract, Section 1, Section 5] The paper repeatedly claims 'The opOL metatheory and case studies are mechanized in Lean 4' and lists Lean mechanization as a contribution, but the submission contains no Lean artifact, no code listing, no link, and no machine-checkable proof. The visible appendix contains paper proofs, not Lean sources. This claim is therefore unverifiable as submitted. Either provide the artifact (and instructions for checking it) or remove/qualify the mechanization claim.
  3. [Theorem 3.1 (Section 3.4)] Theorem 3.1 states that the oblivious semantics refines the adaptive convex powerdomain semantics, and the text says 'To show that result formally'—but no proof appears, and the statement is not accompanied by a specific proof reference. This theorem is used to argue that adaptive proof rules are sound in the oblivious setting. Although Theorem 5.2 is proved directly in Appendices E/F, the missing proof of Theorem 3.1 is still a gap in a stated contribution. Provide a proof or a precise citation to an accessible proof.
minor comments (4)
  1. [Figure 7] Typo: 'Conseqence' should be 'Consequence'.
  2. [Figure 6] The rule label 'SAMP' is inconsistent with the text's 'Samp'; use one style consistently.
  3. [Section 2.3] The phrase 'adversarial choice is an observable effect' is potentially misleading outside the formal model. Consider saying 'observable effect in the model' to emphasize that the model tracks only the schedule index, not timing or other side channels.
  4. [Definition A.2] bits(while e do C end) is an infinite union; it may be worth noting that this is a syntactic over-approximation and that the fixed-point semantics is what the soundness proof actually uses.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: opOL's soundness (Theorem 5.2) is proved by semantic induction against the O monad; the fixed-tape adversary is a modeling premise, not a fitted or predicted input.

full rationale

The derivation chain is not circular. Theorem 5.2 is a soundness theorem proved in Appendices E and F by constructing resource witnesses for each rule relative to the semantic validity predicate in Definition 5.1; the rules (Frame, ND, Prob-Safe, Bounded-Rank) are verified against the denotational model rather than assumed sound. The priv/leak distinction and stability are semantic conditions (Obs_priv, Stablewk), not predicted outputs, and the syntactic tests such as bits(C)={k} are justified by lemmas (e.g. E.1, E.2) rather than by fiat. The paper's citations to Outcome Logic/pcOL are background and comparison; the opOL metatheory is claimed to be mechanized in Lean 4, providing an external check. The only caveat is the modeling premise equating the informal oblivious adversary with a fixed tape where only the current index is observable; this scoping assumption affects transferability to richer threat models but does not make Theorem 5.2 equivalent to its own inputs. No fitted constants, no prediction of fitted data, and no self-citation chain carries the central soundness claim.

Assumptions & free parameters 0 free parameters · 5 assumptions · 2 invented entities

No empirical or physical entities are postulated. The new mathematical structures (oblivious monad, resources) are the machinery of the proof system; they have no falsifiable handle outside the logic itself, but they are defined and used constructively rather than pulled in as unexplained assumptions.

assumptions (5)
  • domain assumption The oblivious adversary is exactly a fixed tape s ∈ Sched = N→N whose entries are consumed in order; any information the adversary has about random outcomes must pass through the current index.
    Section 3.2 defines O(X) this way; if the intended threat model allowed other side channels, the count-tracking independence rules (Frame, ND, NAssign) would not correspond to obliviousness.
  • domain assumption Program values are countable and all distributions are discrete; branching is over countable sets.
    Section 3.1 restricts to countable sets and discrete probability distributions; the fixed-point and direct-sum machinery relies on countable additivity.
  • standard math Standard domain-theoretic facts: D⊥ is a DCPO, Scott-continuous functions have least fixed points, and pointwise extensions preserve pointed DCPOs.
    Used in Section 3.3 to define while-loops as least fixed points via the Kleene fixed-point theorem (Lemma B.4).
  • standard math Measure-theoretic facts about complete probability spaces, product σ-algebras, and conditional probability spaces.
    Section 4.2 builds resources from complete probability spaces and uses product measures for the separating conjunction.
  • domain assumption The adaptive convex powerdomain semantics of Zilberstein et al. 2025b is the correct external benchmark; Theorem 3.1's inclusion relies on that prior definition.
    Theorem 3.1 is stated with a reference to Figure 1 of Zilberstein et al. 2025b; the paper does not re-derive the adaptive semantics from scratch.
invented entities (2)
  • Oblivious monad O(X) = Sched → N → D⊥(X×N)
    purpose: Give denotational semantics for programs with a fixed scheduling tape; outputs pair a value with the updated tape index.
    A new mathematical construct; its adequacy for the informal oblivious-adversary model is argued by examples (Section 2), not by external empirical evidence.
  • Resources R = ⟨P_R, V_R, mem_R, cnt_R⟩
    purpose: Package a probability space with memory footprint and scheduler-count observation, so the logic can track whether randomness is private or leaked.
    A new assertion-semantics object; the count map is the carrier of the paper's privacy/leak distinction.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary." pith.science (2026). https://pith.science/paper/A63F7BA7

@misc{pith2026260716533,
  author       = {Pith},
  title        = {Pith review of: Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/A63F7BA7}},
  note         = {Machine review of arXiv:2607.16533}
}
read the original abstract

In the context of probabilistic programs, an oblivious adversary resolves nondeterminism without seeing the outcomes of random draws. Obliviousness is a common assumption in online algorithms and distributed protocols, but the complex interaction between random draws and adversarial choices makes it challenging to reason about correctness. While there has been significant progress toward reasoning about programs that combine randomization with nondeterminism, most of the work has focused on the adaptive model, whose omniscient view of program state is too powerful to establish correctness for certain classes of programs. We introduce Oblivious Probabilistic Outcome Logic (opOL), a new logic for reasoning about probabilistic programs with nondeterminism controlled by an oblivious adversary. Building on Outcome Logic and Probabilistic Separation Logic, opOL models adversarial choice as a resource and uses probabilistic independence to ensure that random outcomes are hidden from the adversary. The opOL proof system provides expressive and compositional rules for case analysis on both random and nondeterministic outcomes, and for proving almost-sure termination. Expressivity is tested through several case studies, including a paging algorithm and a leader election protocol. The opOL metatheory and case studies are mechanized in Lean 4.

Figures

Figures reproduced from arXiv: 2607.16533 by the authors.

Figure 1
Figure 1. A simple online paging algorithm. 2 Overview Oblivious adversaries were first studied in the context of online algorithms, which process inputs as they arrive. Ben-David et al. [1990] showed that correctness for some randomized online algorithms requires the adversary choosing the inputs to be oblivious, meaning that the adversary cannot see random choices. For example, consider the paging algorithm in [PITH_FULL_I… view at source ↗
Figure 2
Figure 2. Syntax of program commands 𝐶 ∈ Cmd. forms below both state that 𝑎 and 𝑏 are distributed like fair coins, but whereas 𝑎 is unknown to the adversary, 𝑏 may have been leaked, so future adversarial decisions may be correlated with 𝑏. 𝑎 priv ∼ Ber 1 2  𝑏 leak ∼ Ber 1 2  In a nondeterministic program, the Frame rule can only augment the specification with information about private sources of randomness, precluding an un… view at source ↗
Figure 3
Figure 3. Denotational Semantics for programs J·K : Cmd → Mem → O (Mem). a probabilistic choice over the resulting distribution and assigning 𝑥 to the value in each branch. Adversarial choice 𝑥 ← 𝑒 is defined similarly, but uses & to determine which index 𝑖 to take from the list 𝑒. Finally, the semantics of a loop is the least fixed point of the characteristic function Φ⟨𝐶,𝑒 ⟩ from [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figures from the paper (9 more)
Figure 4
Figure 4. Figure 4: Semantics of outcome assertions expressed as satisfaction relation. [PITH_FULL_IMAGE:figures/full_fig_p012_4.png]
Figure 5
Figure 5. Figure 5: Entailment laws for outcome conjunctions and their interaction with separation. [PITH_FULL_IMAGE:figures/full_fig_p016_5.png]
Figure 6
Figure 6. Figure 6: Rules for Sequential Commands. input distribution 𝜇 ∈ D⊥(Mem × N). Fixing the scheduler tape 𝑠, we uncurry J𝐶K as follows: J𝐶K𝑠 : Mem × N → D⊥(Mem × N) J𝐶K𝑠 (𝜎, 𝑛) ≜ J𝐶K (𝜎) (𝑠) (𝑛) Then the D⊥ Kleisli extension J𝐶K † 𝑠 (𝜇) denotes running 𝐶 from 𝜇. Using the new notat…
Figure 7
Figure 7. Figure 7: Structural and Derived Rules. 𝑝 is the probability that the next scheduling bit is even. Since the frame R𝐹 is stable, it contributes no schedule counts, and therefore we have R ⊗ R𝐹 = (R1 ⊗ R𝐹 ) ⊕𝑝 (R2 ⊗ R𝐹 ), and we still know that the left and right operands will ex…
Figure 8
Figure 8. Figure 8: Bounded-Rank Rule. Unlike the splitting rules in pcOL, the opOL variants do not require that the postcondition witnesses a partition of the sample space to satisfy disjointness in the direct sum definition, since we now use probability spaces over an index set rather t…
Figure 9
Figure 9. Figure 9: Semantics of pure separation logic assertions. [PITH_FULL_IMAGE:figures/full_fig_p030_9.png]
Figure 10
Figure 10. Figure 10: Constructor rules for precision, weak stability, and convexity. [PITH_FULL_IMAGE:figures/full_fig_p031_10.png]
Figure 11
Figure 11. Figure 11: Basic entailment laws for outcome assertions. [PITH_FULL_IMAGE:figures/full_fig_p032_11.png]
Figure 13
Figure 13. Figure 13: Resource algebra and distribution-refinement facts used throughout the soundness proof, grouped [PITH_FULL_IMAGE:figures/full_fig_p040_13.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 10 canonical work pages

  1. [1]

    1995.Domain Theory

    Samson Abramsky and Achim Jung. 1995.Domain Theory. Oxford University Press, Inc., USA, 1–168. Krzysztof Apt and Gordon Plotkin

    1995

  2. [2]

    Sequential composition adds consumption, branching forms take unions over possible branches, and nondeterministic choice adds one entry for the branch selection

    bits(𝐶1 &𝐶 2)={1+𝑘|𝑘∈bits(𝐶 1)∪bits(𝐶 2)} bits(while𝑒do𝐶end)={𝑛·𝑘|𝑛∈N, 𝑘∈bits(𝐶)} The base cases distinguish commands that do not query the scheduler from adversarial assign- ment, which consumes one entry. Sequential composition adds consumption, branching forms take unions over possible branches, and nondeterministic choice adds one entry for the branch...

    1995

  3. [13]

    InProgramming Languages and Systems, Viktor Vafeiadis (Ed.)

    A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model. InProgramming Languages and Systems, Viktor Vafeiadis (Ed.). Springer Nature Switzerland, Cham, 322–348. doi:10.1007/978-3-031-91118-7_13 Panagiota Fatourou, Marios Mavronicolas, and Paul Spirakis

    work page doi:10.1007/978-3-031-91118-7_13

  4. [17]

    Formal Specifications: Foundations, Methods, Tools and Applications

    Probabilistic models for the guarded command language.Science of Computer Programming28, 2 (1997), 171–192. Formal Specifications: Foundations, Methods, Tools and Applications. doi:10.1016/S0167-6423(96)00019-6 Claire Jones and Gordon Plotkin

    work page doi:10.1016/s0167-6423(96)00019-6 1997

  5. [20]

    InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Mumbai, India)(POPL ’15)

    Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Mumbai, India)(POPL ’15). Association for Computing Machinery, New York, NY, USA, 637–650. doi:10.1145/2676726.2676980 Klaus Keimel and Gordon Plotkin

    arXiv

  6. [22]

    arXiv:2411.00197 [cs.LO] https://arxiv.org/abs/2411.00197 John M

    Total Outcome Logic: Unified Reasoning for a Taxonomy of Program Logics. arXiv:2411.00197 [cs.LO] https://arxiv.org/abs/2411.00197 John M. Li, Amal Ahmed, and Steven Holtzen

    arXiv

  7. [26]

    doi:10.1007/BF01759073 Annabelle McIver and Carroll Morgan

    A strongly competitive randomized paging algorithm.Algorithmica6, 1–6 (June 1991), 816–825. doi:10.1007/BF01759073 Annabelle McIver and Carroll Morgan. 2005.Abstraction, Refinement and Proof for Probabilistic Systems. Springer. doi:10. 1007/b138392 E. Moggi

    work page doi:10.1007/bf01759073 1991

  8. [27]

    In[1989] Proceedings

    Computational lambda-calculus and monads. In[1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science. 14–23. doi:10.1109/LICS.1989.39155 Eugenio Moggi

    arXiv 1989

Show all 43 references
  1. [28]

    doi:10.1016/0890- 5401(91)90052-4 Rajeev Motwani and Prabhakar Raghavan

    Notions of computation and monads.Information and Computation93, 1 (1991), 55–92. doi:10.1016/0890- 5401(91)90052-4 Rajeev Motwani and Prabhakar Raghavan. 1995.Randomized Algorithms. Cambridge University Press. Leonardo de Moura and Sebastian Ullrich

    1991 doi

  2. [30]

    InCONCUR 2004 - Concurrency Theory

    Resources, Concurrency and Local Reasoning. InCONCUR 2004 - Concurrency Theory. Springer Berlin Heidelberg, Berlin, Heidelberg, 49–67. doi:10.1016/j.tcs.2006.12.035 Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang

    2004 doi

  3. [32]

    Memory versus randomization in on-line algorithms.IBM J. Res. Dev.38, 6 (Nov. 1994), 683–707. doi:10.1147/rd.386.0683 J.C. Reynolds

    1994 doi

  4. [38]

    InProceedings 17th Annual IEEE Symposium on Logic in Computer Science

    The powerdomain of indexed valuations. InProceedings 17th Annual IEEE Symposium on Logic in Computer Science. 299–308. doi:10.1109/LICS.2002.1029838 Noam Zilberstein

    2002 arXiv

  5. [39]

    ACM Trans

    Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects. ACM Trans. Program. Lang. Syst.47, 3, Article 14 (Sept. 2025), 71 pages. doi:10.1145/3743131 Noam Zilberstein, Derek Dreyer, and Alexandra Silva

    2025 doi

  6. [40]

    ACM Program

    Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning.Proc. ACM Program. Lang.7, OOPSLA1, Article 93 (Apr 2023), 29 pages. doi:10.1145/3586045 Noam Zilberstein, Daniele Gorla, and Alexandra Silva. 2025a. Denotational Semantics for Probabilistic and C...

    2023 doi

  7. [41]

    348), Patricia Bouyer and Jaco van de Pol (Eds.)

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 348), Patricia Bouyer and Jaco van de Pol (Eds.). Schloss Dagstuhl – Leibniz-Zentrum f"ur Informatik, Dagstuhl, Germany, 39:1–39:24. doi:10.4230/LIPIcs.CONCUR.2025.39 Noam Zilberstein, Dexter Kozen, Alexandra Sil...

    2025 doi

  8. [43]

    ACM Program

    Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants.Proc. ACM Program. Lang.10, POPL (Jan 2026), 30 pages. doi:10.1145/3776651 Oblivious Probabilistic Outcome Logic 111:29 Appendix A Omitted Definitions 30 A.1 Resource 30 A.2 Asserti...

    2026 doi

  9. [1971]

    Steve Selvin

    Towards a Mathematical Semantics for Computer Languages.Proceedings of the Symposium on Computers and Automata21 (01 1971). Steve Selvin

    1971

  10. [1974]

    doi:10.1007/BF00288637 Lyle A

    Axiomatic Approach to Total Correctness of Programs.Acta Inf.3, 3 (sep 1974), 243–263. doi:10.1007/BF00288637 Lyle A. McGeoch and Daniel D. Sleator

    1974 doi

  11. [1975]

    doi:10.1080/00031305.1975.10479121 Joseph Tassarotti and Robert Harper

    Letters to the Editor.The American Statistician29, 1 (1975), 67–71. doi:10.1080/00031305.1975.10479121 Joseph Tassarotti and Robert Harper

    1975

  12. [1976]

    ACM19, 5 (May 1976), 236–243

    A lattice model of secure information flow.Commun. ACM19, 5 (May 1976), 236–243. doi:10.1145/360051.360056 Weijie Fan, Hongjin Liang, Xinyu Feng, and Hanru Jiang

    1976

  13. [1983]

    InProceedings of the 2nd ACM Symposium on Principles of Distributed Computing(Montreal, Quebec, Canada)(PODC ’83)

    Another advantage of free choice: Completely asynchronous agreement protocols. InProceedings of the 2nd ACM Symposium on Principles of Distributed Computing(Montreal, Quebec, Canada)(PODC ’83). Association for Computing Machinery, New York, NY, USA, 27–30. doi:10.1145/800221.8...

  14. [1985]

    ACM32, 2 (April 1985), 374–382

    Impossibility of distributed consensus with one faulty process.J. ACM32, 2 (April 1985), 374–382. doi:10.1145/3149.214121 David Fremlin. 2001.Measure Theory, Volume

    1985

  15. [1986]

    ACM33, 4 (aug 1986), 724–767

    Countable nondeterminism and random assignment.J. ACM33, 4 (aug 1986), 724–767. doi:10.1145/6490.6494 James Aspnes

    1986

  16. [1989]

    InFourth Annual Symposium on Logic in Computer Science

    A Probabilistic Powerdomain of Evaluations. InFourth Annual Symposium on Logic in Computer Science. 186–195. doi:10.1109/lics.1989.39173 Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer

    1989

  17. [1990]

    InProceedings of the Twenty-Second Annual ACM Symposium on Theory of Computing(Baltimore, Maryland, USA)(STOC ’90)

    On the power of randomization in online algorithms. InProceedings of the Twenty-Second Annual ACM Symposium on Theory of Computing(Baltimore, Maryland, USA)(STOC ’90). Association for Computing Machinery, New York, NY, USA, 379–386. doi:10.1145/100216.100268 Michael Ben-Or

  18. [1991]

    1991), 685–699

    Competitive paging algorithms.Journal of Algorithms12, 4 (Dec. 1991), 685–699. doi:10.1016/0196-6774(91)90041-V Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson

    1991 doi

  19. [1994]

    Comput.23, 4 (1994), 701–712

    Wait-Free Consensus Using Asynchronous Hardware.SIAM J. Comput.23, 4 (1994), 701–712. doi:10.1137/S0097539790192635 Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer

    1994 doi

  20. [1997]

    InProceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing(Santa Barbara, California, USA)(PODC ’97)

    Efficiency of oblivious versus non-oblivious schedulers for optimistic, rate-based flow control (extended abstract). InProceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing(Santa Barbara, California, USA)(PODC ’97). Association for Computing ...

  21. [2001]

    InProceedings of the 15th International Workshop on Computer Science Logic (CSL ’01)

    Local Reasoning about Programs That Alter Data Structures. InProceedings of the 15th International Workshop on Computer Science Logic (CSL ’01). Springer-Verlag, Berlin, Heidelberg, 1–19. doi:10.1007/3-540-44802-0_1 P. Raghavan and M. Snir

    doi

  22. [2004]

    InCONCUR 2004 - Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.)

    A Semantics for Concurrent Separation Logic. InCONCUR 2004 - Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 16–34. doi:10.1007/978-3-540-28644- 8_2 Benny Chor, Amos Israeli, and Ming Li

    2004 doi

  23. [2009]

    Electronic Notes in Theoretical Computer Science222 (2009), 3–99

    Semantic Domains for Combining Probability and Non-Determinism. Electronic Notes in Theoretical Computer Science222 (2009), 3–99. doi:10.1016/j.entcs.2009.01.002 Daniele Varacca

    2009 doi

  24. [2010]

    In Proceedings of the 29th ACM SIGACT-SIGOPS symposium on Principles of distributed computing

    A modular approach to shared-memory consensus, with applications to the probabilistic-write model. In Proceedings of the 29th ACM SIGACT-SIGOPS symposium on Principles of distributed computing. ACM, Zurich Switzerland, 460–467. doi:10.1145/1835698.1835802 James Aspnes

  25. [2012]

    InProceedings of the 2012 ACM Symposium on Principles of Distributed Computing(Madeira, Portugal)(PODC ’12)

    Faster randomized consensus with an oblivious adversary. InProceedings of the 2012 ACM Symposium on Principles of Distributed Computing(Madeira, Portugal)(PODC ’12). Association for Computing Machinery, New York, NY, USA, 1–8. doi:10.1145/2332432.2332434 Steve Awodey. 2006.Cat...

    2012

  26. [2015]

    InAutomated Deduction - CADE-25, Amy P

    The Lean Theorem Prover (System Description). InAutomated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham, 378–388. doi:10.1007/978-3-319-21401-6_26 Dorothy E. Denning

    doi

  27. [2017]

    Mixed powerdomains for probability and nondeterminism.Logical Methods in Computer ScienceVolume 13, Issue 1 (Jan. 2017). doi:10.23638/LMCS-13(1:2)2017 111:28 Hanxi Chen, Noam Zilberstein, Andrew C. Myers, and Alexandra Silva James Li, Noam Zilberstein, and Alexandra Silva

    2017 doi

  28. [2018]

    doi:10.1017/S0956796818000151 Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer

    Iris from the ground up: A modular foundation for higher-order concurrent separation logic.Journal of Functional Programming28 (2018). doi:10.1017/S0956796818000151 Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer

    2018 doi

  29. [2019]

    ACM Program

    A Separation Logic for Concurrent Randomized Programs.Proc. ACM Program. Lang.3, POPL, Article 64 (Jan 2019), 30 pages. doi:10.1145/3290377 Regina Tix, Klaus Keimel, and Gordon Plotkin

    2019 doi

  30. [2020]

    ACM Program

    A Probabilistic Separation Logic.Proc. ACM Program. Lang.4, POPL, Article 55 (Jan. 2020), 30 pages. doi:10.1145/3371123 S. Ben-David, A. Borodin, R. Karp, G. Tardos, and A. Wigderson

    2020 doi

  31. [2021]

    InAutomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings

    The Lean 4 Theorem Prover and Programming Language. InAutomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. Springer-Verlag, Berlin, Heidelberg, 625–635. doi:10.1007/978-3-030-79876-5_37 Peter W. O’Hearn

    2021 doi

  32. [2023]

    ACM Program

    Lilac: A Modal Separation Logic for Conditional Probability.Proc. ACM Program. Lang.7, PLDI, Article 112 (jun 2023), 24 pages. doi:10.1145/3591226 Janine Lohse, Tim Rohde, Jimmy Xin, Niklas Mück, Iona Kuhn, Derek Dreyer, Deepak Garg, and Emanuele D’Osualdo

    2023 doi

  33. [2024]

    ACM Program

    Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects.Proc. ACM Program. Lang.8, OOPSLA1, Article 104 (apr 2024), 29 pages. doi:10.1145/3649821 Noam Zilberstein, Alexandra Silva, and Joseph Tassarotti

    2024 doi

  34. [2025]

    ACM Program

    Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning.Proc. ACM Program. Lang.9, POPL, Article 58 (Jan. 2025), 31 pages. doi:10.1145/3704894 Gilles Barthe, Justin Hsu, and Kevin Liao

    2025 doi

  35. [2026]

    Technical Report

    First Steps Towards Probabilistic Iris: A Separation Logic with Independence, Conditioning, and Dynamic Heap Allocation. Technical Report. Max Planck Institute for Software Systems (MPI-SWS). Accessed: 2026-03-23. https://people.mpi- sws.org/~jlohse/downloads/amaryllis.pdf Zoh...

    2026

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.