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
13:40 - 15:20
|Proving expected sensitivity of probabilistic programs|
|Synthesizing Coupling Proofs of Differential Privacy|
|Measurable cones and stable, measurable functions|
|Denotational validation of higher-order Bayesian inference|
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