Semantics of Higher-order Probabilistic Programs
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.
Sat 23 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
14:00 - 15:30 | |||
14:00 20mTalk | A Lambda-Calculus Foundation for Universal Probabilistic Programming PPS Johannes Borgström Uppsala University, Ugo Dal Lago University of Bologna, Andrew D. Gordon Microsoft Research and University of Edinburgh, Marcin Szymczak University of Edinburgh Pre-print | ||
14:20 10mMeeting | Discussion 5 PPS | ||
14:30 20mTalk | Making our Own Luck: A Language for Random Generators PPS Leonidas Lampropoulos University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Cătălin Hriţcu INRIA Paris, John Hughes Chalmers University of Technology, Zoe Paraskevopoulou Princeton University, Li-yao Xia ENS Paris Pre-print | ||
14:50 10mMeeting | Discussion 6 PPS | ||
15:00 20mTalk | Semantics of Higher-order Probabilistic Programs PPS Sam Staton University of Oxford, Hongseok Yang University of Oxford, UK, Chris Heunen University of Edinburgh, Ohad Kammar University of Cambridge, Frank Wood University of Oxford Pre-print | ||
15:20 10mMeeting | Discussion 7 PPS |