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 JanDisplayed time zone: Tijuana, Baja California change
Fri 12 Jan
Displayed time zone: Tijuana, Baja California change
13:40 - 15:20 | |||
13:40 25mTalk | 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 25mTalk | Synthesizing Coupling Proofs of Differential Privacy Research Papers | ||
14:30 25mTalk | 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 25mTalk | 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 Moss University of Oxford, Chris Heunen University of Edinburgh, Zoubin Ghahramani University of Cambridge | ||