ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 15:30 - 16:00 at SUN II - Program Semantics Chair(s): Andrzej Murawski

We define a new denotational semantics for a first-order probabilistic programming language in terms of probabilistic event structures. This semantics is intensional, meaning that the interpretation of a program contains information about its behaviour throughout execution, rather than a simple distribution on return values. In particular, occurrences of sampling and conditioning are recorded as explicit events, partially ordered according to the data dependencies between the corresponding statements in the program.
This interpretation is adequate: we show that the usual measure-theoretic semantics of a program can be recovered from its event structure representation. Moreover it can be leveraged for MCMC inference: we prove correct a version of single-site Metropolis-Hastings with incremental recomputation, in which the proposal kernel takes into account the semantic information in order to avoid performing some of the redundant sampling.

Tue 9 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 16:00
Program SemanticsESOP at SUN II
Chair(s): Andrzej Murawski University of Oxford
14:00
30m
Talk
Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination
ESOP
Dylan McDermott University of Cambridge, Alan Mycroft University of Cambridge
Link to publication
14:30
30m
Talk
Effectful Normal-Form Bisimulation
ESOP
Ugo Dal Lago University of Bologna / Inria, Francesco Gavazzo
Link to publication
15:00
30m
Talk
On the Multi-Language Construction
ESOP
Samuele Buro Università degli Studi di Verona, Isabella Mastroeni University of Verona, Italy
Link to publication
15:30
30m
Talk
Probabilistic Programming Inference via Intensional Semantics
ESOP
Simon Castellan Imperial College London, UK, Hugo Paquet University of Cambridge
Link to publication