Reasoning About Sampling Without Sampling: Atomic Machines for Contextual Equivalence(…)

on YouTube ↗13m

" summary

Claims an abstract-machine semantics for probabilistic programs that treats sampling as deterministic up to atomic equivalence, using atomic sheaf / forcing semantics (Simpson's atomic logic) to guard states with a source-of-entropy. Builds a guarded SECD-style machine with a new sampling transition, shows random variables form an atomic sheaf and that samples are unique modulo the source-of-entropy symmetries, and uses parametric logical relations to derive contextual equivalences including alpha-style and some privacy equations.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 0:21Abstract machines in probabilistic programming
3. 1:04Fresh names and higher-order equations
4. 2:27Atomic equivalence and Atomic Sheaf Logic
5. 3:50Contextual equivalences in probabilistic programming
6. 5:35Crypto worlds for group two equations
7. 7:01Forcing semantics and Atomic Sheaves
8. 8:25Atomic Sheaf abstract machine
9. 10:30SECD machine with probabilistic sampling
10. 11:12Summary
11. 11:56Q&A