An Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
summary
Mechanization in Coq of an intrinsically-typed first-order probabilistic language with a denotational semantics that returns measures and proves measurability of deterministic expressions and left-totality and right-uniqueness of evaluation. The development uses canonical structures and custom entries to solve context unification, relies on the MComp analysis library for measurable spaces and probability measures, encodes score/normalize and sampling, and demonstrates symbolic evaluation and a commuting-score program transformation that normalizes to the intended distribution.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:25Motivation and contributions
- 3:26SF PPL with intrinsic typing
- 7:04Basic types and contexts in Coq
- 8:49Unification with conical structures
- 12:43SS PPL syntax and semantics
- 15:23MasCComp measures and semantics
- 16:37Syntax to semantics via mutual induction
- 20:00Symbolic evaluation example
- 21:48Conclusion and future work
- 22:30Q&A
related talks
49mSemantic Foundations for Probabilistic Programming
20mVerified Density Compilation for a Probabilistic Programming Language
19mExtensible Metatheory Mechanization via Family Polymorphism
30mRelatively Complete Verification of Probabilistic Programs
22mProbabilistic Refinement Session Types
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
15mStable Relations and Abstract Interpretation of Higher-Order Programs
46mMechanizing Abstract Interpretation