Foundations for typedriven probabilistic modelling
POPL’24 TutorialFest, London, England
Ohad Kammar January 15 2024
The last few years have seen several breakthroughs in the semantic foundations of probabilistic and statistical modelling. In this tutorial, we will use types to introduce, use, and organise abstractions for probabilistic modelling.
We will do so first for discrete probability, and then more generally with the recentlydeveloped quasiBorel spaces. The tutorial is accompanied by exercises for selfstudy, allowing you to develop a working knowledge and handson experience after it.
Course materials
Lectures
All lectures.
Planned structure:
 Motivation
 Typedriven probability and the discrete model
 typedriven probability and the discrete model (part 2)
 events, Borel sets, and measurable spaces
 quasiBorel spaces
 Borel set basics: introductory exercises if you’ve never worked with Borel sets, or looking for a refresher.
 Measurable spaces and functions: exercises exploring the structure of measurable spaces and measurable functions.
 Basic category theory: use these exercises to improve your category theory.
 Aumann’s theorem: consequences of and related concepts to Aumann’s theorem on the inexistence of measurable functionspaces.
 Sequences: examples of higherorder measure theory using sequences.
 QuasiBorel spaces: first acquaintance with quasiBorel spaces.

Extracurricular material
 More on the Borel hierarchy: a guided tour of the proof of Aumann’s theorem.
 Aumann’s theorem for Lebesgue measurablity: extending Aumann’s theorem from Borel measurable functions to Lebesgue measurable functions.
 Simple type structure
 Dependenttype structure
 Standard Borel spaces
 Qbs construction: space combinators — you may want to spread these exercises over several sittings.
 Borel subspaces: measurable subsets in a quasiBorel space.

Measurability by type
 Function spaces: practice the definition of the function space of two qbses, with the Borel subsets and random element spaces.
 Integration
 Random variables
 Conditioning
Getting help and reporting mistakes
Please never hesitate to get in touch. Approach me directly in person during the summer school or by email. You may prefer to ask a question on the #qbs channel on the SPLS Zulip server: spls.zulipchat.com . Others would benefit from your question in that case too!