Universal Semantics for the Stochastic Lambda-Calculus
Pedro Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Michael Roberts

TL;DR
This paper introduces sound and adequate semantics for the stochastic lambda calculus, establishing a formal link between operational and denotational views, and resolving a key open problem in probabilistic higher-order programming.
Contribution
It provides the first adequacy theorem connecting operational and denotational semantics for the stochastic lambda calculus.
Findings
Established sound and adequate semantics for stochastic lambda calculus
Proved an adequacy theorem relating operational and denotational semantics
Resolved a major open problem in probabilistic higher-order programming semantics
Abstract
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Advanced Algebra and Logic
