Ohad's Research - Foundations for Type-Driven Probabilistic Modelling [POPL'24 TutorialFest]

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

Course materials


All lectures.

Planned structure:

  1. Lecture 1a
  • Motivation
  • Type-driven probability and the discrete model
  1. Lecture 1b
  • type-driven probability and the discrete model (part 2)
  • events, Borel sets, and measurable spaces
  • quasi-Borel spaces
Relevant exercise sheets:
  1. Lecture 2a
  • Simple type structure
  • Dependent-type structure
  • Standard Borel spaces
Relevant exercise sheets:
  • Qbs construction: space combinators — you may want to spread these exercises over several sittings.
  • Borel subspaces: measurable subsets in a quasi-Borel space.
  • Measurability by type
    • Function spaces: practice the definition of the function space of two qbses, with the Borel subsets and random element spaces.
  1. Lecture 2b
  • 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!

Previous iterations