New foundations for probabilistic separation logic
summary
Proposes a new separation-logic semantics where propositions are sets of probability spaces and heaps are replaced by probability-space fragments combined with a novel independent combination operator; builds a program logic for Markov kernels with a frame rule identical to the standard one (no extra side conditions on random variables), admits continuous distributions, supports a conditioning modality for conditional independence, and is used to mechanize and verify a nontrivial weighted-sampling algorithm — the logic and proof strategy succeed on that case.
AI-written summary · about
related talks
49mSemantic Foundations for Probabilistic Programming
22mImplementing separation logic using an SMT-backed Frame Rule
21mEmbedding Hindsight Reasoning in Separation Logic
11mIntroduction
13mSemantic Foundations for Laziness in Discrete Probabilistic Programming
24mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
21mOutcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…)
19mCausality and Semantic Separation