Semantics of Probabilistic Programs using S-Finite Kernels in Coq
summary
Extends a Coq formalization of measure and integration by adding s-finite kernels to interpret typing judgments for a probabilistic language, and proves key properties like measurability under composition and stability of kernels by composition. Implements deterministic distributions, conditioning/score semantics, and gives construction rules that connect program syntax to measure-theoretic semantics. The resulting Coq library makes it possible to verify program transformations and reason about execution of probabilistic programs.
AI-written summary · about
chapters (8)
- 0:00Probabilistic semantics in Coq
- 5:44Probabilistic operators in Coq
- 10:12Compositionality of semantics
- 13:08Deterministic terms and conditioning
- 14:40Execution model and satisfaction
- 19:34Mathematical formalization
- 20:45Tutorial and applications
- 22:56Conclusion and Q&A
related talks
49mSemantic Foundations for Probabilistic Programming
21mGuaranteed inference for probabilistic programs: a parallelisable, small-step o...
20mWhat do posterior distributions of probabilistic programs look like?
24mHigher order programming with probabilistic effects: A model of stochastic memo...
14mExact Probabilistic Inference Using Generating Functions
26mPiecewise Analysis of Probabilistic Programs via k-Induction
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming
30mλS: Computable Semantics for Diff'ble Programming with HO Functions and Datatypes