An introduction to statistical modelling semantics with higherorder measure theory
SPLV: The 4th Scottish Programming Languages and Verification Summer School
Ohad Kammar 1116 July 2022
The last few years have seen several breakthroughs in the semantic foundations of statistical modelling. In this course, I will introduce one of these approaches — quasiBorel spaces. We will review and develop a semantic toolkit for measure theory using higherorder functions. The course will be accompanied by exercises and tutorials, allowing you to develop a working knowledge and handson experience.
Course materials
Slides
 All slides (updated with corrections)
 Lectures 12 (video unavailable unfortunately)
 Lectures 34 (video)
See the Marseille course for additional content and videos.
Exercise sheet (under development)

Context and background
Doing all of these exercises is too much for the course, the goal is to learn something new, or — if you already know this material — help someone else learn something new. 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.

An introduction to QuasiBorel spaces
 QuasiBorel spaces: first acquaintance with quasiBorel 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.
 Type structure: use typeformers to put spaces together and form more complex spaces.
 Standard Borel spaces (under development): use measurabilitybytype to construct standard Borel spaces.

Measures and integration (under development)
 Measures: introductory exercises if you’ve never worked with measures before.
 Lebesgue integration: the definition of the Lebesgue integral.
 Randomisable measures: the class of measures we will work with.

Kolmogorov’s conditional expectation (under development)
 Random variable spaces: definition and basic properties of the Lebesgue spaces.
 Geometry of random variable spaces: basic geometric and topological properties of Lebesgue spaces.
 Conditional expectation: existence and almostcertain uniqueness of Kolmogorov’s conditional expectation.

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.