Semantics of Probabilistic Programs Using s-Finite Kernels in Dependent Type Theory

ACM:3732291 · 1 repo reference this paper in their README

Probabilistic programming languages are used to write probabilistic models to make probabilistic inferences. A number of rigorous semantics have been developed to reason about transformations of probabilistic programs and their execution. We propose to investigate the formalization of such a semantics to allow for the formal verification of probabilistic programs. Concretely, we extend an existing formalization of measure and integration theory in the Rocq prover, a proof assistant based on dependent type theory, with s-finite kernels, a mathematical structure to interpret typing judgments in the semantics of a probabilistic programming language. We explain the issues raised by organizing kernels as a hierarchy of mathematical structures and use the latter to formalize the semantics of a first-order probabilistic programming language. We use this semantics to establish generic properties of this language, prove rewriting laws to perform symbolic evaluation, and reason about iteration.