Tue 9 Jan 2018 11:30 - 12:00 at Bradbury - SESSION II (3 talks) Chair(s): Erik Meijer

Probabilistic programming systems are infamously difficult to test. Most properties of interest only hold probabilistically, and so on any particular set of runs a correct implementation may produce unexpected output while an incorrect implementation may produce the expected output. To make matters worse, the expected output is rarely known in the first place. While a small subset of a probabilistic programming language may permit exact inference by other means, most of the complexity in a probabilistic programming system will likely only apply to programs that make use of more sophisticated language features, such as branching and recursion. There may be no way to know a priori how inference is supposed to behave on such programs. We show how developers can avoid empirical testing altogether and simply prove that their probabilistic programming systems behave correctly on all inputs using tools from software verification and formal mathematics.

Tue 9 Jan
Times are displayed in time zone: Tijuana, Baja California change

10:30 - 12:00: SESSION II (3 talks) PPS at Bradbury
Chair(s): Erik Meijer
10:30 - 11:00
The semantic structure of quasi-Borel spaces: algebra, logic, and recursion
Chris HeunenUniversity of Edinburgh, Ohad KammarUniversity of Oxford, Sean K. MossUniversity of Cambridge, Adam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Sam StatonUniversity of Oxford, Matthijs VákárUniversity of Oxford, Hongseok YangUniversity of Oxford
11:00 - 11:30
Stable, measurable functions and probabilistic programs
Michele PaganiUniversity Paris Diderot, Thomas EhrhardCNRS and University Paris Diderot, Christine TassonUniversity Paris Diderot
11:30 - 12:00
Formal Methods For Probabilistic Programming
Daniel SelsamStanford University