Abstract

Synchronous languages are now a standard industrial tool for critical embedded systems. Designers write high-level specifications by composing streams of values using block diagrams. These languages have been extended with Bayesian reasoning to program state-space models which compute a stream of distributions given a stream of observations [1].

This talk aims at describing semantics for probabilistic synchronous languages, based on a joint work with Guillaume Baudart and Louis Mandel [2]. The key idea is to interpret probabilistic expressions as a stream of non-normalized density functions which maps random variable values to a result and a positive score. Two equivalent semantics are presented: the co-iterative semantics is executable while the relational semantics is easy to use for proving program equivalence. The semantical framework is applied to prove the correctness of a program transformation required to run an optimized inference algorithm.

[1] Reactive Probabilistic Programming, Guillaume Baudart et al, PLDI 2020 [2] Scheduled agnostic Semantics for Reactive Probabilistic Programming, Guillaume Baudart, Louis Mandel, Christine Tasson, ACM Transactions on Probabilistic Machine Learning 2025