Measurable Cones and Stable, Measurable Functions

Abstract

We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives a denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We prove the soundness and adequacy of this model with respect to a call-by-name operational semantics and give some examples of its denotations.

References in corpus (3)

• Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
• A Convenient Category for Higher-Order Probability Theory
• Mixed powerdomains for probability and nondeterminism

Cited by in corpus (9)

• A Domain Theory for Statistical Probabilistic Programming
• Formal verification of higher-order probabilistic programs
• ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
• Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere
• A Monad for Probabilistic Point Processes
• Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
• Concrete categories and higher-order recursion (With applications including probability, differentiability, and full abstraction)
• Linear logic in normed cones: probabilistic coherence spaces and beyond
• A Cartesian Closed Category for Random Variables