Modular Specifications and Implementations of Random Samplers in Higher-Order Separation(…)
summary
Defines a reusable distribution typeclass for Eris (Iris-based) that internalizes sampler reasoning, proves a distribution adequacy theorem linking the logical credit rule to the actual output distribution, and equips samplers with presampling tapes to decouple sampling from program flow. Implements and machine-verifies samplers for binomial, geometric (almost-sure termination via error induction), and beta-binomial distributions, provides proofs and artifacts (Zenodo/DOI), and demonstrates the approach works end-to-end.
AI-written summary · about
chapters (10)
- 0:00Probabilistic programs intro
- 1:48ERIS and randomness
- 3:37Adequacy theorems
- 5:45Reasoning principles for samplers
- 8:37Presampling tapes
- 11:28Lazy sampling with tapes
- 12:52Bernoulli distribution labeling
- 15:02Geometric distribution case study
- 17:51Conclusions and future work
- 18:56Q&A
related talks
01h 02mSampling for Linear Algebra, Statistics, and Optimization II
29mTesting Probability Distributions using Conditional Samples
20mWhat do posterior distributions of probabilistic programs look like?
01h 26mStreaming, Sketching and Sufficient Statistics II
29mProbabilistic Programming: What It Is and How It Works
45mTBD
43mPrivacy Amplification by Sampling in Practice
01h 04mNonparametric Bayesian Methods: Models, Algorithms, and Applications II