Fri 12 Jan 2018 14:30 - 14:55 at Watercourt - Probability Chair(s): Lars Birkedal

We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives the first denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We prove the soundness and adequacy of this model with respect to a call-by-name operational semantics and give some examples of its denotations.

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

13:40 - 15:20
ProbabilityResearch Papers at Watercourt
Chair(s): Lars Birkedal Aarhus University
13:40
25m
Talk
Proving expected sensitivity of probabilistic programs
Research Papers
Gilles Barthe IMDEA Software Institute, Thomas Espitau Universite Pierre et Marie Curie, Benjamin Gregoire INRIA, Justin Hsu University College London, Pierre-Yves Strub Ecole Polytechnique
14:05
25m
Talk
Synthesizing Coupling Proofs of Differential Privacy
Research Papers
Aws Albarghouthi University of Wisconsin-Madison, Justin Hsu University College London
14:30
25m
Talk
Measurable cones and stable, measurable functions
Research Papers
Thomas Ehrhard CNRS and University Paris Diderot, Michele Pagani University Paris Diderot, Christine Tasson University Paris Diderot
14:55
25m
Talk
Denotational validation of higher-order Bayesian inference
Research Papers
Adam Ścibior University of Cambridge and MPI Tuebingen, Ohad Kammar University of Oxford, Matthijs Vákár University of Oxford, Sam Staton University of Oxford, Hongseok Yang University of Oxford, Yufei Cai University of Tuebingen, Klaus Ostermann University of Tuebingen, Sean K. Moss University of Cambridge, Chris Heunen University of Edinburgh, Zoubin Ghahramani University of Cambridge