Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic

Watch this 23-minute conference presentation from CPP 2026 that introduces a methodology for specifying and implementing random samplers using higher-order separation logic. Learn how researchers Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, and Lars Birkedal address the challenge of creating modular, reusable specifications for probabilistic programs that generate samples from complex distributions using primitive uniform samplers. Discover their approach using Eris, a probabilistic program logic based on Iris separation logic, and explore how they develop a distribution typeclass that abstracts the requirements for concrete distribution implementations while providing reasoning principles for client code. Examine practical applications of this methodology through implementations of classical distributions including binomials, geometrics, and beta-binomials, and understand how this work advances formal verification techniques for probabilistic programming by enabling both correctness proofs and expressive client reasoning.