Semantics of Probabilistic Programs: An Algebraic Approach

The following summary was generated by AI from the slides.

This talk presents an algebraic approach to the semantics and static analysis of probabilistic programs structured around two results: a hyper-path denotational semantics for low-level probabilistic programs with nondeterminism using Markov algebras (MFPS’19), which gives a domain-theoretic account of nondeterminism-first vs. nondeterminism-last resolution; and the PMAF interprocedural dataflow framework (PLDI’18), which instantiates the algebra to recover Bayesian inference and Markov decision problems as existing analyses while enabling a new expectation-invariant analysis via a relational polyhedral domain. Together, the two results establish Markov algebras as a unifying semantic and algorithmic foundation for quantitative reasoning about probabilistic programs.