Write a Blog >>
Wed 22 Jan 2020 11:13 - 11:35 at Ile de France II (IDF II) - Probabilistic Programming Chair(s): Alexandra Silva

We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs a la Scott through the use of ordered Banach spaces which allow definitions in terms of fixed points. Our semantics is a model of intuitionistic linear logic: it is linear because it is based on a symmetric monoidal closed category of ordered Banach spaces, but by constructing an exponential comonad we can also accommodate non-linear reasoning. We apply our semantics to the verification of the classical Gibbs sampling algorithm.

Semantics of Higher-Order Probabilistic Programs with Conditioning (POPL_2020.pdf)221KiB

Wed 22 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
Probabilistic ProgrammingResearch Papers at Ile de France II (IDF II)
Chair(s): Alexandra Silva University College London
10:30
21m
Talk
Towards Verified Stochastic Variational Inference for Probabilistic Programs
Research Papers
Wonyeol Lee KAIST, Hangyeol Yu KAIST, Xavier Rival INRIA/CNRS/ENS Paris, Hongseok Yang KAIST
Link to publication DOI Media Attached
10:51
21m
Talk
Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
Research Papers
Alexander K. Lew Massachusetts Institute of Technology, USA, Marco Cusumano-Towner MIT-CSAIL, Benjamin Sherman Massachusetts Institute of Technology, USA, Michael Carbin Massachusetts Institute of Technology, Vikash K. Mansinghka MIT
Link to publication DOI Media Attached
11:13
21m
Talk
Semantics of Higher-Order Probabilistic Programs with Conditioning
Research Papers
Fredrik Dahlqvist University College London, Dexter Kozen Cornell University
Link to publication DOI Media Attached File Attached