[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.