Principles of Programming Seminar

— 4:30pm

In Person - Gates Hillman 8102

OHAD KAMMAR , Senior Research Fellow, Laboratory for the Foundations of Computer Science, School of Informatics, University of Edinburgh

Type-driven foundations for statistical modelling

The classical foundation for statistical modelling takes as primitive the notion of an observable event, axiomatising their properties by measurable spaces and functions. While measurable spaces support concrete type structure well, one faces inherent no-go results when dealing with more abstract spaces like: spaces of measurable functions for modelling continuous-time processes; spaces of measurable functionals for measurable statistics; and measurably-dependent function spaces for conditional probabilities. In joint work with Heunen, Staton, and Yang, we proposed quasi-Borel spaces. Here the axiomatisation takes as primitive the notion of a random element, also known as random variables in concrete cases. These spaces support notions for both concrete and abstract spaces. Having arrived at this collection of spaces in a fairly abstract manner, as a full sub-category of concrete sheaves, I was pleasantly surprised to find that some of their abstract type structure does support operations at the heart of statistics, measure theory, and classical descriptive set theory. 

In this talk, I will survey this line of work. I will cover the basic definitions and ideas underlying quasi-Borel spaces, as well as some abstract ones. I will then review how myself and others have usedthese spaces as a semantic foundation for expressive probabilistic modelling languages and their Monte Carlo Bayesian inference implementations. I will conclude with more recent work developing and applying the dependently typed structure of these spaces. 


Ohad Kammar is a Senior Research Fellow in the Laboratory for the Foundations of Computer Science at the University of Edinburgh School of Informatics. He is interested in programming language theory and design, algebra, logic, and category theory. 

Faculty Host: Jan Hoffman

Event Website:

Add event to Google
Add event to iCal