Semantics for Reactive Probabilistic Programming

Explore a technical lecture that delves into the semantics of probabilistic synchronous languages, focusing on their application in critical embedded systems and Bayesian reasoning. Learn how synchronous languages have evolved as industry tools, allowing designers to create high-level specifications through stream value composition. Discover the extension of these languages into Bayesian reasoning for programming state-space models that process observation streams into distribution streams. Examine two key semantic interpretations of probabilistic expressions: the executable co-iterative semantics and the relational semantics used for program equivalence proofs. Understand how probabilistic expressions are interpreted as streams of un-normalized density functions, mapping random variable values to results and positive scores. Follow the application of this semantical framework in proving the correctness of program transformations necessary for optimized inference algorithm implementation, based on collaborative research with Guillaume Baudart and Louis Mandel.