Semantic Foundations for Probabilistic Programming
summary
Develops a denotational semantics for an idealized Anglican (a Church fork) that supports continuous distributions, higher-order functions, soft constraints via score/observe, normalization and recursion. Uses measurable spaces and kernels, then embeds into sheaves and a new quasi-measurable spaces cartesian-closed universe (extends the Giry-style monad) so function types exist; first-order terms remain ordinary measurable maps. Proves correctness of transformations used in practice (SMC unrolling, importance sampling, conjugate-prior rewrites) and gives conditions for normalization errors.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:04Semantic foundations
- 4:23Probabilistic programming
- 7:24Higher-order functions
- 12:29Language mechanics
- 17:11Formalizing the language
- 23:39Verification of transformations
- 28:29Advanced mathematical modeling
- 36:24Recursion and conclusion
- 44:06Q&A session
related talks
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
13mSemantic Foundations for Laziness in Discrete Probabilistic Programming
24mSemantics of Probabilistic Programs using S-Finite Kernels in Coq
24mHigher order programming with probabilistic effects: A model of stochastic memo...
05mNew foundations for probabilistic separation logic
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
30mRelatively Complete Verification of Probabilistic Programs
19mTowards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic