A Convenient Category for Higher-Order Probability Theory

Chris Heunen, Ohad Kammar, Sam Staton, Hongseok Yang

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization 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. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.
Original languageEnglish
Title of host publication2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages12
ISBN (Electronic)978-1-5090-3018-7
ISBN (Print)978-1-5090-3019-4
Publication statusPublished - 18 Aug 2017
Event2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science - Reykjavik, Reykjavik, Iceland
Duration: 20 Jun 201723 Jun 2017

Publication series

NameIEEE Symposium on Logic in Computer Science
ISSN (Electronic)1043-6871


Conference2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2017
Internet address

Fingerprint Dive into the research topics of 'A Convenient Category for Higher-Order Probability Theory'. Together they form a unique fingerprint.

Cite this