Ohad's Research - Foundations for Type-Driven Probabilistic Modelling [LSS@ANU]

Foundations for type-driven 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 recently-developed quasi-Borel spaces. The course is accompanied by exercises, allowing you to develop a working knowledge and hands-on 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


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 function-spaces.
    • Sequences: examples of higher-order measure theory using sequences.
  • An introduction to Quasi-Borel spaces
  • 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 type-formers to put spaces together and form more complex spaces.
    • Standard Borel spaces (under development): use measurability-by-type 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 almost-certain uniqueness of Kolmogorov’s conditional expectation.
  • Extra-curricular material

Invited Tutorial at Logic of Probabilistic Programming 2022