Foundations for typedriven probabilistic modelling
LSS@ANU: Logic Summer School at Australian National University
Ohad Kammar 4 December – 15 December 2023
The last few years have seen several breakthroughs in the semantic foundations of probabilistic and statistical modelling. In this course, 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 course is accompanied by exercises, allowing you to develop a working knowledge and handson experience during the summer school and after it.
Course materials
The 2023 edition is still under development. In the meanwhile, you can look at previous editions of this course:
Previous edition: Scottish PL and Verification Summer School
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.