pith. machine review for the scientific record. sign in

arxiv: 2605.13765 · v1 · submitted 2026-05-13 · 💻 cs.LO · cs.PL

Recognition: no theorem link

First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation

Janine Lohse , Tim Rohde , Jimmy Xin , Niklas M\"uck , Iona Kuhn , Derek Dreyer , Deepak Garg , Emanuele D'Osualdo
Authors on Pith no claims yet

Pith reviewed 2026-05-14 17:44 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords probabilistic separation logicdynamic allocationindependenceconditioningIrismechanized verificationresource algebrasRocq
0
0 comments X

The pith

Amaryllis is the first general-purpose probabilistic logic to support independence, conditioning, and dynamic memory allocation.

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

The paper presents Amaryllis as a new general-purpose probabilistic logic that integrates independence and conditioning with dynamic heap allocation. Existing logics could not handle pointers because memory configurations differ across probabilistic branches. Amaryllis uses an indexed valuation model to lift Iris-style resource ownership to probability distributions. This allows adapting core Iris mechanisms like frame-preserving updates and weakest preconditions to probabilistic reasoning. All results are mechanized in the Rocq proof assistant with an Iris-based proof mode.

Core claim

Amaryllis establishes a sound integration of probabilistic assertions with dynamic allocation by means of an indexed valuation-style model, which promotes standard Iris resource ownership to the distributional level, and adapts frame-preserving updates, authoritative resource algebras, and the weakest precondition modality to validate independence, conditioning, and heap operations.

What carries the argument

The indexed valuation-style model of probabilistic assertions, which enables generic promotion of Iris-style resource ownership to the level of distributions.

If this is right

  • Programs involving probabilistic choice and dynamic memory allocation can now be verified using modular independence and conditioning assertions.
  • Iris-style ghost state and resource algebras become available for probabilistic program reasoning.
  • Frame-preserving updates and weakest preconditions are sound in the presence of probability distributions over heaps.
  • Mechanized proofs of such programs are possible within a proof assistant using the provided Iris-based proof mode.

Where Pith is reading between the lines

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

  • This approach may extend to incorporating concurrency or other advanced Iris features into probabilistic settings.
  • Verification of algorithms using randomized data structures like hash tables or dynamic graphs could become feasible.
  • Similar indexed models might be applied to other separation logics to add probabilistic capabilities.

Load-bearing premise

The indexed valuation-style model integrates soundly with Iris-style resource algebras without losing the properties of independence or conditioning.

What would settle it

A concrete program with dynamic allocation whose probabilistic semantics permits an independence or conditioning violation that Amaryllis claims to rule out would falsify the soundness result.

Figures

Figures reproduced from arXiv: 2605.13765 by Deepak Garg, Derek Dreyer, Emanuele D'Osualdo, Iona Kuhn, Janine Lohse, Jimmy Xin, Niklas M\"uck, Tim Rohde.

Figure 1
Figure 1. Figure 1: Selected proof rules of Amaryllis show the definitions of ∗, −∗ and . (𝑃 ∗ 𝑄) (𝑥) ≜ ∃𝑥1, 𝑥2. 𝑥1 · 𝑥2 ≼ 𝑥 ∧ 𝑃 (𝑥1) ∧ 𝑄(𝑥2) (𝑃 −∗ 𝑄) (𝑥) ≜ ∀𝑥 ′ . V (𝑥 · 𝑥 ′ ) ∧ 𝑃 (𝑥 ′ ) ⇒ 𝑄(𝑥 · 𝑥 ′ ) ( 𝑃) (𝑥) ≜ 𝑃 (|𝑥 |) It can be shown that all connectives preserve the almost-sure upwards-closedness of pProp. Entail￾ment can be defined in the standard way 𝑃 ⊢ 𝑄 ≜ ∀𝑥. V (𝑥) ⇒ 𝑃 (𝑥) ⇒ 𝑄(𝑥) In the following, we instantiate 𝑀 w… view at source ↗
Figure 2
Figure 2. Figure 2: Selected proof rules about weakest preconditions [PITH_FULL_IMAGE:figures/full_fig_p017_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Proof rules for conditioning A.1 Example Proofs Here we write down the details of the derivation that we used for the Markov blanket example in Section 6.2 [PITH_FULL_IMAGE:figures/full_fig_p025_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Proof rules for C-frameable wp-bind wp 𝐸  𝑉 . wp 𝐾[𝑉 ] {Φ} [PITH_FULL_IMAGE:figures/full_fig_p026_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: WP rules We define 𝜇0 ≜ 𝜇1 𝜅2. Following Bayes’ theorem, we define 𝜇2 ≜ 𝜆𝑣2. Í 𝑣1 𝜇0 (𝑣1, 𝑣2) and 𝜅1𝑣2 ≜ 𝜆𝑣1. 𝜇0 (𝑣1,𝑣2 ) 𝜇2 (𝑣2 ) such that we can invert the conditional probability: 𝜇1  𝜅2 (𝑣1, 𝑣2) = 𝜇2  𝜅1 (𝑣2, 𝑣1). We use this equality together with c-transf and derive the following [PITH_FULL_IMAGE:figures/full_fig_p026_5.png] view at source ↗
read the original abstract

There has recently been exciting progress in the realm of *probabilistic separation logics*. An important subclass of these -- including PSL, Lilac, Bluebell, and pcOL -- are *general-purpose probabilistic logics* (or GPLs, for short), meaning that they provide primitive Hoare-style assertions about probability distributions on the program state, along with powerful modularity principles like *independence* and *conditioning*. However, none of these logics support reasoning about dynamically allocated memory (i.e., pointers into a heap), let alone the more sophisticated resource algebra-based ghost state of modern separation logics like Iris. We argue that this is due to a fundamental obstacle: since the shape of memory (and identity of memory locations) may differ under different random outcomes, it is unclear how pointer ownership can be harmonized with probabilistic independence and conditioning. Furthermore, none of the existing GPLs have been mechanized in a proof assistant. In this paper, we take a substantial first step towards a marriage of GPLs and modern separation logics like Iris, in the form of **Amaryllis**. Amaryllis is the first GPL to support independence and conditional reasoning while also handling dynamic memory allocation. To overcome the aforementioned obstacle, we propose a new *indexed valuation*-style model of probabilistic assertions, whereby ownership of a standard Iris-style resource (e.g., heaps) can be promoted to ownership at the level of distributions in a generic fashion. We then show how to adapt the central Iris notions of *frame-preserving update*, *authoritative resource algebras*, and the *weakest precondition modality* to be sound for probabilistic reasoning and validate dynamic allocation. Finally, we have mechanized all our results in the Rocq proof assistant and developed an Iris-based proof mode for conducting proofs within Amaryllis.

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

0 major / 3 minor

Summary. The paper introduces Amaryllis, the first general-purpose probabilistic logic (GPL) supporting independence and conditioning together with dynamic heap allocation. It proposes an indexed valuation-style model that lifts Iris-style resource algebras (including heaps) to distributions over states, adapts frame-preserving updates, authoritative resource algebras, and the weakest-precondition modality to the probabilistic setting, and mechanizes the entire development—including an Iris-based proof mode—in the Rocq proof assistant.

Significance. If the mechanized soundness claims hold, the work constitutes a substantial advance by bridging existing GPLs (PSL, Lilac, Bluebell, pcOL) with modern separation-logic infrastructure. The machine-checked adaptation of Iris primitives and validation of independence/conditioning rules under dynamic allocation are particular strengths, as they discharge the central modeling challenge without ad-hoc parameters or circular reuse.

minor comments (3)
  1. [Abstract] Abstract: the sentence claiming Amaryllis is 'the first GPL to support independence and conditional reasoning while also handling dynamic memory allocation' should be qualified with a forward reference to the related-work discussion in §1 to avoid appearing overstated.
  2. [§4] §4 (or wherever the proof-mode tactics are described): the development of the Iris-based proof mode is mentioned but receives no concrete examples or discussion of proof size or automation effectiveness; adding a small illustrative derivation would strengthen the usability claim.
  3. [§3] Notation: the distinction between the indexed valuation model and the lifted resource algebra is sometimes blurred in prose; a short table contrasting the two (e.g., how ownership and composition are defined at each level) would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our paper, recognition of Amaryllis as the first GPL supporting dynamic heap allocation together with independence and conditioning, and the recommendation for minor revision. We will incorporate presentational improvements in the revised manuscript.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper introduces a new indexed valuation-style model that lifts Iris-style resource algebras to distributions while preserving key properties. All central definitions, including adaptations of frame-preserving updates, authoritative composition, and the weakest-precondition modality, are mechanized in Rocq. Soundness proofs are machine-checked and do not reduce to fitted parameters, self-definitional equations, or load-bearing self-citations. The derivation chain is self-contained via formal verification rather than circular reuse of prior results.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The claim rests on the soundness of the new indexed valuation model and the probabilistic adaptations of Iris concepts; these are mechanized but the abstract provides no independent external benchmarks.

axioms (1)
  • standard math Standard properties of probability distributions and separation logic resource algebras from Iris
    The paper builds on existing Iris framework assumptions for resource ownership and updates.
invented entities (1)
  • Indexed valuation-style model of probabilistic assertions no independent evidence
    purpose: To promote ownership of standard Iris-style resources to the level of distributions while supporting dynamic allocation
    Newly introduced to overcome the obstacle that memory shape may differ under different random outcomes.

pith-pipeline@v0.9.0 · 5657 in / 1130 out tokens · 23891 ms · 2026-05-14T17:44:48.247271+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

37 extracted references · 32 canonical work pages

  1. [1]

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

    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, 284–316. doi: 10.1145/3674635

    work page doi:10.1145/3674635 2024

  2. [2]

    Amal Ahmed. 2004. Semantics of types for mutable state . Ph.D. Dissertation. Princeton University

    2004

  3. [3]

    First Steps Towards Probabilistic Iris: A Separation Logic with Independence, Conditioning, and Dynamic Heap Allocation

    Anonymous. 2026. Rocq development of "First Steps Towards Probabilistic Iris: A Separation Logic with Independence, Conditioning, and Dynamic Heap Allocation". (Jan. 2026). https://zenodo.org/records/18327732?preview=1&token=e yJhbGciOiJIUzUxMiJ9.eyJpZCI6IjFhNGVhZDMyLWNjMzMtNGFmOS05MzMyLTg2NGQ3NDkyNjNlMyIsImRhd GEiOnt9LCJyYW5kb20iOiJjZmJkYmZjNTI0MmQ1ZDQ4N...

    work page arXiv 2026

  4. [4]

    Appel and David A

    Andrew W. Appel and David A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. TOPLAS, 23, 5, 657–683. doi: 10.1145/504709.504712

    work page doi:10.1145/504709.504712 2001

  5. [5]

    Jialu Bao, Emanuele D’Osualdo, and Azadeh Farzan. 2025. Bluebell: an alliance of relational lifting and independence for probabilistic reasoning. Proc. ACM Program. Lang., 9, POPL, 1719–1749. doi: 10.1145/3704894

    work page doi:10.1145/3704894 2025

  6. [6]

    Jialu Bao, Simon Docherty, Justin Hsu, and Alexandra Silva. 2021. A bunched logic for conditional independence. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021 . IEEE, 1–14. doi: 10.1109/LICS52264.2021.9470712

    work page doi:10.1109/lics52264.2021.9470712 2021

  7. [7]

    Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. An assertion-based program logic for probabilistic programs. In Programming Languages and Systems . Springer Interna- tional Publishing, Cham, 117–144

    2018

  8. [8]

    Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub. 2015. Relational reasoning via probabilistic coupling. In Springer, 387–401. doi: 10.1007/978-3-662-48899-7_27

    work page doi:10.1007/978-3-662-48899-7_27 2015

  9. [9]

    Gilles Barthe, Justin Hsu, and Kevin Liao. 2020. A probabilistic separation logic. Proc. ACM Program. Lang., 4, POPL, 55:1–55:30. doi: 10.1145/3371123

    work page doi:10.1145/3371123 2020

  10. [10]

    Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang. , 3, POPL, 34:1–34:29. doi: 10.1145/3290347

    work page doi:10.1145/3290347 2019

  11. [11]

    12 Johannes Borgström, Ugo Dal Lago, Andrew D

    Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. 2016. A lambda-calculus foundation for universal probabilistic programming. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 . Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, (Eds.) ACM, 33–4...

    work page doi:10.1145/2951913.2951942 2016

  12. [12]

    26 Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G

    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, 753–784. doi: 10.1145/3632868

    work page doi:10.1145/3632868 2024

  13. [13]

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

    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, 1196–1226. doi: 10.1145/3704877

    work page doi:10.1145/3704877 2025

  14. [14]

    Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal

    Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal. 2024. Tachis: higher-order separation logic with credits for expected costs. Proc. ACM Program. Lang., 8, OOPSLA2, 1189–1218. doi: 10.1145/3689753

    work page doi:10.1145/3689753 2024

  15. [15]

    Shing Hin Ho, Nicolas Wu, and Azalea Raad. 2026. Bayesian separation logic: a logical foundation and axiomatic semantics for probabilistic programming. Proc. ACM Program. Lang., 10, POPL, Article 54, (Jan. 2026), 29 pages. doi: 10.1145/3776696

    work page doi:10.1145/3776696 2026

  16. [16]

    Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP, 256–269. doi: 10.1145/2951913.2951943

    work page doi:10.1145/2951913.2951943 2016

  17. [17]

    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. JFP, 28, e20. doi: 10.1017/S09567 96818000151

    work page doi:10.1017/s09567 2018

  18. [18]

    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 POPL, 637–650. 24 J. Lohse, T. Rohde, J. Xin, N. Mück, I. Kuhn, D. Dreyer, D. Garg, and E. D’Osualdo

    2015

  19. [19]

    Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest precondition reasoning for expected run-times of probabilistic programs. In ESOP (LNCS). Vol. 9632. Springer, 364–389. doi: 10.1007/978-3-662-49498-1\_15

    work page doi:10.1007/978-3-662-49498-1 2016

  20. [20]

    Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2018. Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM, 65, 5, 30:1–30:68. doi: 10.1145/3208102

    work page doi:10.1145/3208102 2018

  21. [21]

    Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. Mosel: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang., 2, ICFP, 77:1–77:30. doi: 10.1145/3236772

    work page doi:10.1145/3236772 2018

  22. [22]

    Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Informatics Appl., 46, 3, 413–450. doi: 10.1051/ITA/2012012

    work page doi:10.1051/ita/2012012 2012

  23. [23]

    Li, Amal Ahmed, and Steven Holtzen

    John M. Li, Amal Ahmed, and Steven Holtzen. 2023. Lilac: A modal separation logic for conditional probability. Proc. ACM Program. Lang., 7, PLDI, 148–171. doi: 10.1145/3591226

    work page doi:10.1145/3591226 2023

  24. [24]

    Equivalence and conditional independence in atomic sheaf logic

    John M. Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, and Steven Holtzen. 2024. A nominal approach to probabilistic separation logic. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024. Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, (Eds.) ACM, 55:1–55:14. doi: 10.1145/36...

    work page doi:10.1145/3661814.3662135 2024

  25. [25]

    Haselwarter, Joseph Tassarotti, and Lars Birkedal

    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

  26. [26]

    Rupak Majumdar and V. R. Sathiyanarayana. 2025. Sound and complete proof rules for probabilistic termination. Proc. ACM Program. Lang., 9, POPL, 1871–1902. doi: 10.1145/3704899

    work page doi:10.1145/3704899 2025

  27. [27]

    Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems . Monographs in Computer Science. Springer. isbn: 978-0-387-40115-7. doi: 10.1007/B138392

    work page doi:10.1007/b138392 2005

  28. [28]

    O’Hearn, John C

    Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. In Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings (Lecture Notes in Computer Science). Laurent Fribourg, (Ed.) Vol. 2142. Springer, 1–...

    work page doi:10.1007/3-540-44802-0 2001

  29. [29]

    Norman Ramsey and Avi Pfeffer. 2002. Stochastic lambda calculus and monads of probability distributions. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002 . John Launchbury and John C. Mitchell, (Eds.) ACM, 154–165. doi: 10.1145/50 3272.503288

    work page doi:10.1145/50 2002

  30. [30]

    Reynolds

    John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings . IEEE Computer Society, 55–74. doi: 10.1109/LICS.2002.1029817

    work page doi:10.1109/lics.2002.1029817 2002

  31. [31]

    Joseph Tassarotti and Robert Harper. 2019. A separation logic for concurrent randomized programs. Proc. ACM Program. Lang., 3, POPL, 64:1–64:30. doi: 10.1145/3290377

    work page doi:10.1145/3290377 2019

  32. [32]

    Daniele Varacca and Glynn Winskel. 2006. Distributing probability over non-determinism. Math. Struct. Comput. Sci. , 16, 1, 87–113. doi: 10.1017/S0960129505005074

    work page doi:10.1017/s0960129505005074 2006

  33. [33]

    Pengbo Yan, Toby Murray, Olga Ohrimenko, Van-Thuan Pham, and Robert Sison. 2025. Combining classical and probabilistic independence reasoning to verify the security of oblivious algorithms. InFormal Methods. André Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, (Eds.) Springer Nature Switzerland, Cham, 188–205. isbn: 978-3-031-71162-6

    2025

  34. [34]

    Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti. 2025. A demonic outcome logic for random- ized nondeterminism. Proc. ACM Program. Lang., 9, POPL, 539–568. doi: 10.1145/3704855

    work page doi:10.1145/3704855 2025

  35. [35]

    Noam Zilberstein, Angelina Saliling, and Alexandra Silva. 2024. Outcome separation logic: local reasoning for correctness and incorrectness with computational effects. Proc. ACM Program. Lang., 8, OOPSLA1, 276–304. doi: 10.1145/3649821

    work page doi:10.1145/3649821 2024

  36. [36]

    Noam Zilberstein, Alexandra Silva, and Joseph Tassarotti. 2026. Probabilistic concurrent reasoning in outcome logic: independence, conditioning, and invariants. Proc. ACM Program. Lang., 10, POPL

    2026

  37. [37]

    Maaike Zwart and Dan Marsden. 2019. No-go theorems for distributive laws. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019 . IEEE, 1–13. doi: 10.1109/LICS.2019 .8785707. A Proof Rules We give a list of proof rules in this section. The proof rules for conditioning can be found in figure 3, f...

    work page doi:10.1109/lics.2019 2019