[CPP'26] Modular Specifications and Implementations of Random Samplers in Higher-Order Separation(…) скачать в хорошем качестве

[CPP'26] Modular Specifications and Implementations of Random Samplers in Higher-Order Separation(…)

Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic (Video, CPP 2026) Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, Lars Birkedal (ENS Rennes, France; ENS Paris-Saclay, France; Aarhus University, Denmark; Aarhus University, Denmark) Abstract: Probabilistic programs have a myriad of applications, from randomized algorithms to statistical modeling, and as such have inspired a long tradition of probabilistic program logics to verify their correctness. One essential use of probabilistic programs is to program new samplers from more primitive samplers, e.g., to generate samples from more complex distributions only given a primitive uniform sampler. Such samplers are an ideal case study for probabilistic program logics, to ensure that they implement the target distributions correctly. But proving correctness is often not enough, one also wants to reason about clients of these samplers, which require their specifications to be expressive and reusable. In this work, we propose a methodology for giving specifications to samplers that are detailed enough to prove that they are correct, and expressive enough to reason about their clients. We propose our methodology for Eris, a recent probabilistic program logic based on the Iris separation logic. We identify what makes the proof rules and reasoning principles for primitive distributions in Eris work, and we distill them into a distribution typeclass. This presents at an abstract level the requirements that a concrete implementation of a target distribution should satisfy, and provides reasoning principles for clients of the interface. Working at this level of abstraction allows us to prove correctness results, as well as to derive additional reasoning principles for all implementations that adhere to the typeclass interface. We instantiate this approach to a variety of samplers for classical distributions, such as binomials, geometrics and beta-binomials. Article: https://doi.org/10.1145/3779031.3779109 Supplementary archive: https://doi.org/10.5281/zenodo.17800602 (Badges: Artifacts Available) ORCID: https://orcid.org/0009-0005-9568-4592, https://orcid.org/0009-0007-7559-1326, https://orcid.org/0000-0001-6746-2734, https://orcid.org/0000-0003-1320-0098 Video Tags: Probabilistic Programming, Separation Logic, Formal Verification, doi:10.1145/3779031.3779109, doi:10.5281/zenodo.17800602, orcid:0009-0005-9568-4592, orcid:0009-0007-7559-1326, orcid:0000-0001-6746-2734, orcid:0000-0003-1320-0098, Artifacts Available Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2... Sponsored by ACM SIGPLAN.