Probabilistic Programming Semantics for Name Generation

arXiv2007.08638MaRDI QIDQ6345262FDOQ6345262

Michael Wolman, Sam Staton, Dario Stein, Marcin Sabok

Publication date: 16 July 2020

Abstract: We make a formal analogy between random sampling and fresh name generation. We show that quasi-Borel spaces, a model for probabilistic programming, can soundly interpret Stark's $u$-calculus, a calculus for name generation. Moreover, we prove that this semantics is fully abstract up to first-order types. This is surprising for an 'off-the-shelf' model, and requires a novel analysis of probability distributions on function spaces. Our tools are diverse and include descriptive set theory and normal forms for the $u$-calculus.

This page was built for publication: Probabilistic Programming Semantics for Name Generation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6345262)