Lilac: A Modal Separation Logic for Conditional Probability

Explore a 19-minute video presentation from the PLDI 2023 conference introducing Lilac, a novel separation logic for reasoning about probabilistic programs. Delve into how Lilac's separating conjunction captures probabilistic independence, drawing inspiration from an analogy with mutable state where sampling corresponds to dynamic allocation. Discover how probability spaces over a fixed, ambient sample space are presented as natural analogues of heap fragments, and learn about a new combining operation that allows probability spaces to behave like heaps and measurability of random variables to behave like ownership. Examine how this combining operation forms the basis for the model of separation, resulting in a logic with desirable properties, including a frame rule identical to the ordinary one and accommodation of advanced features like continuous random variables and reasoning about quantitative program properties. Investigate a proposed new modality based on disintegration theory for reasoning about conditional probability, and see how the resulting modal logic validates examples from prior work. Gain insights into the formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.

[PLDI'23] Lilac: A Modal Separation Logic for Conditional Probability