Write a Blog >>
Sat 23 Jan 2016 14:00 - 14:20 at Room St Petersburg II - Session 3 Chair(s): Mitchell Wand

We develop the operational semantics of a probabilistic lambda- calculus with continuous distributions, as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of lambda-calculus to the continuous case, via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distributional semantics. Our second contribution is to formalize the implementation technique of trace MCMC for our calculus and to show correctness. A key step is defining a sampling semantics of a term as a function from a trace of random samples to a value, and showing that the distribution induced by integrating over all traces equals the distributional semantics. Another step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distributional semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language.

Sat 23 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

14:00 - 15:30
Session 3PPS at Room St Petersburg II
Chair(s): Mitchell Wand Northeastern University
14:00
20m
Talk
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
10m
Meeting
Discussion 5
PPS

14:30
20m
Talk
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
10m
Meeting
Discussion 6
PPS

15:00
20m
Talk
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
10m
Meeting
Discussion 7
PPS