Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints

We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. This involves measure theory, stochastic labelled transition systems, and functor categories, but admits intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.Categories and Subject Descriptors CR-number [D.3]: Programming languages

• Publication year

  2016

• Venue

  Logic in Computer Science

• Publication date

  2016-01-19

• Fields of study

  Mathematics, Computer Science, Engineering

• Identifiers
  DOI 10.1145/2933575.2935313arXiv 1601.04943
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• BASIC CONCEPTS OF ENRICHED CATEGORY THEORY

  2022cited by this paper
• A lambda-calculus foundation for universal probabilistic programming

  2015cited by this paper
• On computability and disintegration

  2015cited by this paper
• A Provably Correct Sampler for Probabilistic Programs

  2015cited by this paper
• Symbolic Bayesian Inference by Lazy Partial Evaluation

  2015cited by this paper
• Practical probabilistic programming with monads

  2015cited by this paper
• Venture: a higher-order probabilistic programming platform with programmable inference

  2014cited by this paper
• A Compilation Target for Probabilistic Programming Languages

  2014cited by this paper
• Probabilistic coherence spaces are fully abstract for probabilistic PCF

  2014cited by this paper
• A New Approach to Probabilistic Programming Inference

  2014influential reference
• I and J

  2012cited by this paper
• Noncomputable Conditional Distributions

  2011influential reference
• Measure Transformer Semantics for Bayesian Machine Learning

  2011cited by this paper
• A Categorical Approach to Probability Theory

  2010cited by this paper
• PyMC: Bayesian Stochastic Modelling in Python.

  2010cited by this paper
• Computable de Finetti measures

  2009cited by this paper
• A stochastic programming perspective on nonparametric Bayes

  2008cited by this paper
• A probabilistic language based on sampling functions

  2008cited by this paper
• Church: a language for generative models

  2008cited by this paper
• Stochastic Relations : Foundations for Markov Transition Systems

  2007cited by this paper
• Generic models for computational effects

  2006cited by this paper
• Modelling environments in call-by-value programming languages

  2003cited by this paper
• Stochastic lambda calculus and monads of probability distributions

  2002cited by this paper
• Categorical logic

  2001cited by this paper
• Sequential Monte Carlo Methods in Practice

  2001cited by this paper
• Adequacy for Algebraic Effects

  2001cited by this paper
• Call-by-Push-Value: A Subsuming Paradigm

  1999cited by this paper
• A Course on Borel Sets

  1998cited by this paper
• Integration in Real PCF

  1996cited by this paper
• In: Handbook of Logic in Computer Science

  1995cited by this paper
• Notions of Computation and Monads

  1991cited by this paper
• A probabilistic powerdomain of evaluations

  1989cited by this paper
• Type Algebras, Functor Categories, and Block Structure

  1986cited by this paper
• Semantics of probabilistic programs

  1979cited by this paper
• Monads on symmetric monoidal closed categories

  1970cited by this paper
• On type *-algebras

  1967cited by this paper
• Borel structures for function spaces

  1961influential reference

• The Magmoid of Normalized Stochastic Kernels

  2025cites this paper
• Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops

  2025cites this paper
• Open Questions about Time and Self-reference in Living Systems

  2025cites this paper
• Cancellative Convex Semilattices

  2025cites this paper
• On the Relevance of Logic for Artificial Intelligence, and the Promise of Neurosymbolic Learning

  2025influential citation
• Schedule Agnostic Semantics for Reactive Probabilistic Programming

  2025cites this paper
• Semantics of Probabilistic Programs Using s-Finite Kernels in Dependent Type Theory

  2025cites this paper
• Multi-Language Probabilistic Programming

  2025influential citation
• Partial Markov Categories

  2025cites this paper
• The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

  2025cites this paper
• Parallelizable Feynman-Kac Models for Universal Probabilistic Programming

  2025cites this paper
• A Simple Formal Language for Probabilistic Decision Problems

  2024cites this paper
• Language-Agnostic Static Analysis of Probabilistic Programs

  2024cites this paper
• Evidential Decision Theory via Partial Markov Categories

  2023cites this paper
• Automatic Alignment in Higher-Order Probabilistic Programming Languages

  2023cites this paper
• Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing

  2023cites this paper
• Semantics of Probabilistic Programs using s-Finite Kernels in Coq

  2023cites this paper
• Omnisemantics: Smooth Handling of Nondeterminism

  2023cites this paper
• Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving

  2023cites this paper
• A Fibrational Tale of Operational Logical Relations

  2023cites this paper
• Beyond Bayesian Model Averaging over Paths in Probabilistic Programs with Stochastic Support

  2023cites this paper
• Logic + probabilistic programming + causal laws

  2023cites this paper
• Density-Based Semantics for Reactive Probabilistic Programming

  2023cites this paper
• Symbolic Semantics for Probabilistic Programs (extended version)

  2023cites this paper
• Deterministic stream-sampling for probabilistic programming: semantics and verification

  2023cites this paper
• Lilac: A Modal Separation Logic for Conditional Probability

  2023cites this paper
• : PURE, EFFECTFUL

  2023cites this paper
• Declarative Probabilistic Logic Programming in Discrete-Continuous Domains

  2023cites this paper
• Open Higher-Order Logic

  2023cites this paper
• Probabilistic Programming Languages: Independent Choices and Deterministic Systems

  2022cites this paper
• Open Higher-Order Logic (Long Version)

  2022cites this paper
• On Feller continuity and full abstraction

  2022cites this paper
• Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference

  2022cites this paper
• Distribution Theoretic Semantics for Non-Smooth Differentiable Programming

  2022cites this paper
• Nonparametric Involutive Markov Chain Monte Carlo

  2022cites this paper
• A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems

  2022cites this paper
• Higher-Order Generalization Bounds: Learning Deep Probabilistic Programs via PAC-Bayes Objectives

  2022influential citation
• Mixed Nondeterministic-Probabilistic Automata

  2022cites this paper
• Fully abstract models for effectful λ-calculi via category-theoretic logical relations

  2022cites this paper
• Reasoning about “reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recursion

  2022cites this paper
• Commutative Monads for Probabilistic Programming Languages

  2021cites this paper
• Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs

  2021cites this paper
• Multinomial and Hypergeometric Distributions in Markov Categories

  2021cites this paper
• Hierarchical Sampler for Probabilistic Programs via Separation of Control and Data

  2021cites this paper
• Interpreting Lambda Calculus in Domain-Valued Random Variables

  2021cites this paper
• probKanren: A Simple Probabilistic Extension for microKanren

  2021cites this paper
• Multinomial and Hypergeometric Distributions in Markov Categories

  2021cites this paper
• Double Glueing over Free Exponential: with Measure Theoretic Applications

  2021cites this paper
• Expectation Programming

  2021cites this paper
• A Domain-theoretic Approach to Statistical Programming Languages

  2021cites this paper
• Compiling Stan to generative probabilistic languages and extension to deep probabilistic programming

  2021cites this paper
• Supermartingales, Ranking Functions and Probabilistic Lambda Calculus

  2021cites this paper
• Weakest Preexpectation Semantics for Bayesian Inference

  2020cites this paper
• Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages

  2020cites this paper
• Planning as Inference in Epidemiological Dynamics Models

  2020cites this paper
• Presenting convex sets of probability distributions by convex semilattices and unique bases

  2020cites this paper
• Finding the maximum-a-posteriori behaviour of agents in an agent-based model

  2020cites this paper
• Successor-Invariant First-Order Logic on Classes of Bounded Degree

  2020cites this paper
• λPSI: exact inference for higher-order probabilistic programs

  2020cites this paper
• Probabilistic programming semantics for name generation

  2020cites this paper
• A Logic to Reason about Dependence and Independence

  2020cites this paper
• Probabilistic Programs with Stochastic Conditioning

  2020cites this paper
• Probabilistic concurrent game semantics

  2020cites this paper
• Universal Semantics for the Stochastic Lambda-Calculus

  2020cites this paper
• On the Versatility of Open Logical Relations

  2020cites this paper
• A Bunched Logic for Conditional Independence

  2020cites this paper
• Universal Semantics for the Stochastic λ-Calculus

  2020cites this paper
• Termination Analysis of Probabilistic Programs with Martingales

  2020cites this paper
• Probabilistic Programs as Measures

  2020cites this paper
• Planning as Inference in Epidemiological Models

  2020cites this paper
• Synthetic topology in Homotopy Type Theory for probabilistic programming

  2019cites this paper
• Hijacking Malaria Simulators with Probabilistic Programming

  2019cites this paper
• Probabilistic Programming Inference via Intensional Semantics

  2019cites this paper
• Algorithmic Improvisation

  2019cites this paper
• Formally justified and modular Bayesian inference for probabilistic programs

  2019cites this paper
• The Random Conditional Distribution for Higher-Order Probabilistic Inference

  2019cites this paper
• Semantics of higher-order probabilistic programs with conditioning

  2019cites this paper
• Approximations in Probabilistic Programs

  2019influential citation
• A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism

  2019cites this paper
• Termination of Nondeterministic Probabilistic Programs

  2019cites this paper
• DyVerSe – Dynamic Versatile Semantics

  2019cites this paper
• Usability of Probabilistic Programming Languages

  2019cites this paper
• Towards verified stochastic variational inference for probabilistic programs

  2019influential citation
• Compositional Inference Metaprogramming with Convergence Guarantees

  2019cites this paper
• Etalumis: Bringing Probabilistic Programming to Scientific Simulators at Scale

  2019cites this paper
• Deployable probabilistic programming

  2019cites this paper
• On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice

  2019influential citation
• Trace types and denotational semantics for sound programmable inference in probabilistic languages

  2019cites this paper
• Artificial Intelligence and Synthesis in Ecology and Evolution

  2019cites this paper
• Artificial Intelligence for Ecological and Evolutionary Synthesis

  2019cites this paper
• A Linear Exponential Comonad in s-finite Transition Kernels and Probabilistic Coherent Spaces

  2019cites this paper
• Optimal approximate sampling from discrete probability distributions

  2019cites this paper
• Weakest Preexpectation Semantics for Bayesian Inference - Conditioning, Continuous Distributions and Divergence

  2019cites this paper
• The Theory of Traces for Systems with Nondeterminism, Probability, and Termination

  2018cites this paper
• Fine-Grained Semantics for Probabilistic Programs

  2018influential citation
• The Logical Essentials of Bayesian Reasoning

  2018cites this paper
• S-finite Kernels and Game Semantics for Probabilistic Programming

  2018cites this paper
• From probability monads to commutative effectuses

  2018cites this paper
• Borel Kernels and their Approximation, Categorically

  2018influential citation
• Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus

  2018cites this paper