For about an year or so, we have been working on the semantics of higher-order probabilistic programming languages that support continuous distributions, such as Church, Venture and Anglican. Our goal was to verify the correctness of program optimisations that we developed for Anglican, and to understand unusual programming concepts in Anglican, such as nested query and distribution object. Defining the semantics of such a language turns out to be very challenging because the combination of higher-order functions and continuous distributions poses a nontrivial technical problem. In order to handle continuous distributions properly, we need to use tools from measure theory, but the standard setting of measure theory lacks a proper notion of function space: the category of measurable spaces is not cartesian closed. After a lot of struggles with this problem, we learnt that abstract tools from category theory can be used to resolve this problem and to lead to a semantics of a call-by-value higher-order probabilistic programming language with continuous distributions. Our two-page abstract below contains a summary of our findings. We plan to (and hope to) give a more accessible presentation of the work in PPS’16.

This is joint work with Sam Staton, Chris Heunen, Ohad Kammar and Frank Wood.

The abstract is available here: semantics-higher-order-ppl