Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
This program is tentative and subject to change.
We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behaviour of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In Bluebell, we unify these styles of reasoning through the introduction of a new modality we call “joint conditioning” that can encode and illuminate the rich interaction between conditional independence and relational liftings; the two powerhouses from the two styles of reasoning.
This program is tentative and subject to change.
Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change
10:40 - 12:00 | |||
10:40 20mTalk | Inference Plans for Hybrid Particle Filtering POPL Ellie Y. Cheng MIT, Eric Atkinson , Guillaume Baudart Inria, Louis Mandel IBM Research, USA, Michael Carbin Massachusetts Institute of Technology | ||
11:00 20mTalk | Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops POPL Pre-print | ||
11:20 20mTalk | Modelling Recursion and Probabilistic Choice in Guarded Type Theory POPL Philipp Stassen Aarhus University, Rasmus Ejlers Møgelberg IT University of Copenhagen, Maaike Annebet Zwart IT University of Copenhagen, Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University | ||
11:40 20mTalk | Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning POPL Jialu Bao Cornell University, Emanuele D'Osualdo University of Konstanz, Azadeh Farzan University of Toronto |