Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning

This conference talk presents Bluebell, a program logic that innovatively combines unary and relational reasoning styles for probabilistic programs. Discover how the researchers from Cornell University, MPI-SWS/University of Konstanz, and University of Toronto have created a unified approach through a new "joint conditioning" modality that bridges conditional independence and relational liftings. Learn about the powerful interaction between these two reasoning paradigms, where unary-style reasoning offers expressiveness through independence and conditioning mechanisms, while relational reasoning excels at comparing similar programs without characterizing individual output distributions. The presentation explores applications in deductive verification and areas like differential privacy, demonstrating how Bluebell illuminates the rich interplay between these previously separate reasoning approaches. This 22-minute talk was delivered at the POPL 2025 conference (January 19-25, 2025) and is sponsored by ACM SIGPLAN.