Probabilistic programming semantics for name generation

Abstract: I will discuss a recent result connecting the nu-calculus (which is an extension of simply-typed lambda calculus modelling the so-called "name generation") with a recent model for probabilistic programming, called the quasi-Borel spaces. There is a natural interpretation of the nu-calculus in quasi-Borel spaces and our main result says that this interpretation is fully abstract up to first-order types, which means that if two first-order terms are observationally equivalent, then the associated elements of quasi-Borel spaces are the same. This is joint work with Sam Staton, Dario Stein and Michael Wolman. In this talk, I will not assume any prior knowledge of lambda calculus or models of probabilistic programming.