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
Times are displayed in time zone: Tijuana, Baja California change

13:40 - 15:20: ProbabilityResearch Papers at Watercourt
Chair(s): Lars BirkedalAarhus University
13:40 - 14:05
Talk
Proving expected sensitivity of probabilistic programs
Research Papers
Gilles BartheIMDEA Software Institute, Thomas EspitauUniversite Pierre et Marie Curie, Benjamin GregoireINRIA, Justin HsuUniversity College London, Pierre-Yves StrubEcole Polytechnique
14:05 - 14:30
Talk
Synthesizing Coupling Proofs of Differential Privacy
Research Papers
Aws AlbarghouthiUniversity of Wisconsin-Madison, Justin HsuUniversity College London
14:30 - 14:55
Talk
Measurable cones and stable, measurable functions
Research Papers
Thomas EhrhardCNRS and University Paris Diderot, Michele PaganiUniversity Paris Diderot, Christine TassonUniversity Paris Diderot
14:55 - 15:20
Talk
Denotational validation of higher-order Bayesian inference
Research Papers
Adam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Ohad KammarUniversity of Oxford, Matthijs VákárUniversity of Oxford, Sam StatonUniversity of Oxford, Hongseok YangUniversity of Oxford, Yufei CaiUniversity of Tuebingen, Klaus OstermannUniversity of Tuebingen, Sean K. MossUniversity of Cambridge, Chris HeunenUniversity of Edinburgh, Zoubin GhahramaniUniversity of Cambridge