Semantics of higher-order probabilistic programs with continuous distributions

Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory does not handle higher-order functions well: the category of measurable spaces is not cartesian closed.

In this talk, I will explain my joint work with Chris Heunen, Ohad Kammar and Sam Staton that aims at addressing this semantic challenge. I will introduce quasi-Borel spaces, and show that these spaces: form a new formalisation of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. If time permits, I will also briefly explain the use of quasi-Borel spaces for higher-order functions and probability.