ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Tue 14 Apr 2015 11:30 - 12:00 at Skeel - Session 1 Chair(s): Jan Vitek

Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other uses such as rare event simulation and probabilistic verification, except that all such probabilistic languages are necessarily limited because they are defined or implemented in terms of an impoverished theory of probability. Measure-theoretic probability provides a more general foundation, but its generality makes finding computational content difficult. We develop a measure-theoretic semantics for a first-order probabilistic language with recursion, which interprets programs as functions that compute preimages. Preimage functions are generally uncomputable, so we derive an approximating semantics. We implement the approximating semantics and use the implementation to carry out Bayesian inference, stochastic ray tracing, and probabilistic verification of floating-point error bounds.

Tue 14 Apr

Displayed time zone: Azores change

10:30 - 12:30
Session 1ESOP at Skeel
Chair(s): Jan Vitek Northeastern University
10:30
30m
Talk
Probabilistic Programs as Spreadsheet Queries
ESOP
Andrew D. Gordon Microsoft Research and University of Edinburgh, Claudio Russo Microsoft Research, Marcin Szymczak University of Edinburgh, Johannes Borgström Uppsala University, Nicolas Rolland Microsoft Research, Thore Graepel Microsoft Research, Daniel Tarlow Microsoft Research
11:00
30m
Talk
Static Analysis of Spreadsheet Applications for Type-Unsafe Operations Detection
ESOP
Tie Cheng CNRS, ENS, INRIA, Paris, France, Xavier Rival INRIA/CNRS/ENS Paris
11:30
30m
Talk
Running Probabilistic Programs Backwards
ESOP
Neil Toronto Brigham Young University, Jay McCarthy , David Van Horn
12:00
30m
Talk
A Verified Compiler for Probability Density Functions
ESOP
Manuel Eberl Technische Universität München, Johannes Hölzl Technische Universität München, Tobias Nipkow Technische Universität München