Tue 20 Jun 2023 13:40 - 14:00 at Royal - PLDI: Probabilistic Analyses Chair(s): Gagandeep Singh

We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. Inspired by an analogy with mutable state where sampling corresponds to dynamic allocation, we show how probability spaces over a fixed, ambient sample space appear to be the natural analogue of heap fragments, and present a new combining operation on them such that probability spaces behave like heaps and measurability of random variables behaves like ownership. This combining operation forms the basis for our model of separation, and produces a logic with many pleasant properties. In particular, Lilac has a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs. Then we propose a new modality based on disintegration theory for reasoning about conditional probability. We show how the resulting modal logic validates examples from prior work, and give a formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.

Tue 20 Jun

Displayed time zone: Eastern Time (US & Canada) change

13:40 - 15:40
PLDI: Probabilistic AnalysesPLDI Research Papers at Royal
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign

#pldi-tue-1340-probabilistic-royal Discord icon small YouTube icon small

13:40
20m
Talk
Lilac: A Modal Separation Logic for Conditional Probability
PLDI Research Papers
John Li Northeastern University, Amal Ahmed Northeastern University, USA, Steven Holtzen Northeastern University
DOI Pre-print
14:00
20m
Talk
Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning
PLDI Research Papers
Alexander Bagnall Ohio University, Gordon Stewart Bedrock Systems, Anindya Banerjee IMDEA Software Institute
DOI
14:20
20m
Talk
Verified Density Compilation for a Probabilistic Programming Language
PLDI Research Papers
Joseph Tassarotti NYU, Jean-Baptiste Tristan Amazon Web Services
DOI
14:40
20m
Talk
Probabilistic Programming with Stochastic Probabilities
PLDI Research Papers
Alexander K. Lew Massachusetts Institute of Technology, Matin Ghavami Massachusetts Institute of Technology, Martin Rinard MIT, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI
15:00
20m
Talk
Automated Expected Value Analysis of Recursive Programs
PLDI Research Papers
Martin Avanzini Inria, Georg Moser University of Innsbruck, Michael Schaper Build Informed
DOI
15:20
20m
Talk
Synthesizing Quantum-Circuit Optimizers
PLDI Research Papers
Amanda Xu University of Wisconsin-Madison, Abtin Molavi University of Wisconsin-Madison, Lauren Pick University of Wisconsin-Madison and University of California, Berkeley, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison
DOI Pre-print