Probabilistic programming semantics for name generation

Journal article

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 the ν-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 ν-calculus.

Authors: Sabok, M; Staton, S; Stein, D; Wolman, M

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Association for Computing Machinery
• Journal: Proceedings of the ACM on Programming Languages
• Volume: 5
• Issue: POPL
• Article number: 11
• Publication date: 2021-01-04
• Acceptance date: 2020-10-01
• DOI: 10.1145/3434292
• EISSN: 2475-1421
• Language: English
• Keywords: name generation; descriptive set theory; FFR; probabilistic programming; synthetic probability theory; standard Borel spaces; nu-calculus; denotational semantics; Borel on Borel; quasi-Borel spaces