Universal Semantics for the Stochastic λ-Calculus
Pedro H. Azevedo de Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden, Michael Roberts
2021Year
5Citations
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 an explicit source of randomness to reason about higher-order probabilistic programs.
The function Fun 2 is injective:
We define Lam 2 to be the inverse of Fun 2 on the image of Fun 2 . Thus
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 13ff4e71-1e3a-4728-970b-64db791d8e21Builds on1
Related papers
- Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic ChoiceAlejandro Aguirre, Lars BirkedalPOPL 2023 · 13 citations
- Full abstraction for the quantum lambda-calculusPierre Clairambault, Marc de VismePOPL 2020 · 25 citations
- Trace types and denotational semantics for sound programmable inference in probabilistic languagesAlexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin et al.POPL 2020 · 30 citations
- Deterministic stream-sampling for probabilistic programming: semantics and verificationFredrik Dahlqvist, Alexandra Silva, William SmithLICS 2023 · 4 citations
- Probabilistic programming semantics for name generationMarcin Sabok, Sam Staton, Dario Stein, Michael WolmanPOPL 2021 · 2 citations
