arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Author

Sam Staton

79 papers · 2002–2026

2002: 12003: 02004: 12005: 02006: 12007: 02008: 22009: 12010: 12011: 52012: 12013: 52014: 52015: 02016: 22017: 62018: 52019: 42020: 52021: 72022: 42023: 62024: 22025: 72026: 8
2002peak 8 in 20262026

Frequent co-authors

Papers

showing 1–25 of 79 RSS

A Convenient Category for Higher-Order Probability Theory

Chris Heunen, Ohad Kammar, Sam Staton +1 more

cs.PL · · cited 191× · arXiv ↗ · more like this ·

Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory does not handle higher-order functions well: the category of measurable spaces is not cartesian closed. Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of…

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

Sam Staton, Hongseok Yang, Chris Heunen +2 more

cs.PL · · cited 149× · arXiv ↗ · more like this ·

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. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit 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…

Relating coalgebraic notions of bisimulation

Sam Staton

cs.LO · · cited 120× · arXiv ↗ · more like this ·

The theory of coalgebras, for an endofunctor on a category, has been proposed as a general theory of transition systems. We investigate and relate four generalizations of bisimulation to this setting, providing conditions under which the four different generalizations coincide. We study transfinite sequences whose limits are the greatest bisimulations.

Semantics for probabilistic programming

Sam Staton, Hongseok Yang, Frank Wood +2 more

Artificial Intelligence · · cited 112× · DOI ↗ · more like this ·

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…

A Domain Theory for Statistical Probabilistic Programming

Matthijs Vákár, Ohad Kammar, Sam Staton

cs.LO · · cited 95× · arXiv ↗ · more like this ·

We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on `quasi-Borel predomains'. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with…

Denotational validation of higher-order Bayesian inference

Adam Ścibior, Ohad Kammar, Matthijs Vákár +7 more

cs.PL · · cited 78× · arXiv ↗ · more like this ·

We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. We show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics. Semantic accounts of continuous distributions use measurable spaces. However, our use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with…

W2951670568

Matthijs Vákár, Ohad Kammar, Sam Staton

Artificial Intelligence · Oxford University Research Archive (ORA) (University of Oxford) · · cited 37× · OpenAlex ↗ · more like this ·

<p>We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity.</p> <p>Our new semantic model is based on `quasi-Borel predomains'. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be…

Name-passing process calculi: operational models and structural operational semantics

Sam Staton

Artificial Intelligence · CL Technical Reports · · cited 36× · DOI ↗ · more like this ·

This thesis is about the formal semantics of name-passing process calculi. We study operational models by relating various different notions of model, and we analyse structural operational semantics by extracting a congruence rule format from a model theory. All aspects of structural operational semantics are addressed: behaviour, syntax, and rule-based inductive definitions. A variety of models for name-passing behaviour are considered and developed. We relate classes of indexed labelled transition systems, proposed by Cattani and Sewell, with coalgebraic models proposed by Fiore and Turi. A general notion of structured coalgebra is introduced and developed, and a natural notion of structured bisimulation is related to Sangiorgi’s open bisimulation for the π-calculus. At first the state spaces are organised as presheaves, but it is reasonable to constrain the models to sheaves in a…

A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics

Marcelo Fiore, Sam Staton

Artificial Intelligence · · cited 36× · DOI ↗ · more like this ·

We introduce a mathematical structural operational semantics that yields a congruence result for bisimilarity and is suitable for investigating rule formats for name-passing systems. Indeed, we instantiate this general abstract model theory in a framework of nominal sets and extract from it a GSOS-like rule format for name-passing process calculi for which the associated notion of behavioural equivalence - given by a form of open bisimilarity - is a congruence

Compositional Semantics for Probabilistic Programs with Exact Conditioning

Dario Stein, Sam Staton

cs.PL · · cited 33× · arXiv ↗ · more like this ·

We define a probabilistic programming language for Gaussian random variables with a first-class exact conditioning construct. We give operational, denotational and equational semantics for this language, establishing convenient properties like exchangeability of conditions. Conditioning on equality of continuous random variables is nontrivial, as the exact observation may have probability zero; this is Borel's paradox. Using categorical formulations of conditional probability, we show that the good properties of our language are not particular to Gaussians, but can be derived from universal properties, thus generalizing to wider settings. We define the Cond construction, which internalizes conditioning as a morphism, providing general compositional semantics for probabilistic programming with exact conditioning.

Linear usage of state

Rasmus Ejlers Møgelberg, Sam Staton

cs.PL · · cited 33× · arXiv ↗ · more like this ·

We investigate the phenomenon that "every monad is a linear state monad". We do this by studying a fully-complete state-passing translation from an impure call-by-value language to a new linear type theory: the enriched call-by-value calculus. The results are not specific to store, but can be applied to any computational effect expressible using algebraic operations, even to effects that are not usually thought of as stateful. There is a bijective correspondence between generic effects in the source language and state access operations in the enriched call-by-value calculus. From the perspective of categorical models, the enriched call-by-value calculus suggests a refinement of the traditional Kleisli models of effectful call-by-value languages. The new models can be understood as enriched adjunctions.

Affine Monads and Lazy Structures for Bayesian Programming

Swaraj Dash, Younesse Kaddar, Hugo Paquet +1 more

cs.PL · · cited 31× · arXiv ↗ · more like this ·

We show that streams and lazy data structures are a natural idiom for programming with infinite-dimensional Bayesian methods such as Poisson processes, Gaussian processes, jump processes, Dirichlet processes, and Beta processes. The crucial semantic idea, inspired by developments in synthetic probability theory, is to work with two separate monads: an affine monad of probability, which supports laziness, and a commutative, non-affine monad of measures, which does not. (Affine means that $T(1)\cong 1$.) We show that the separation is important from a decidability perspective, and that the recent model of quasi-Borel spaces supports these two monads. To perform Bayesian inference with these examples, we introduce new inference methods that are specially adapted to laziness; they are proven correct by reference to the Metropolis-Hastings-Green method. Our theoretical development is…

ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs

Alexander K. Lew, Mathieu Huot, Sam Staton +1 more

cs.PL · · cited 29× · arXiv ↗ · more like this ·

Optimizing the expected values of probabilistic processes is a central problem in computer science and its applications, arising in fields ranging from artificial intelligence to operations research to statistical computing. Unfortunately, automatic differentiation techniques developed for deterministic programs do not in general compute the correct gradients needed for widely used solutions based on gradient-based optimization. In this paper, we present ADEV, an extension to forward-mode AD that correctly differentiates the expectations of probabilistic processes represented as programs that make random choices. Our algorithm is a source-to-source program transformation on an expressive, higher-order language for probabilistic computation, with both discrete and continuous probability distributions. The result of our transformation is a new probabilistic program, whose expected return…

Classical Control and Quantum Circuits in Enriched Category Theory

Mathys Rennela, Sam Staton

Artificial Intelligence · Electronic Notes in Theoretical Computer Science · · cited 23× · DOI ↗ · more like this ·

We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for the host language is standard, and involves cartesian closed categories and monads. We interpret the circuit language not in an ordinary category, but in a category that is enriched in the host category. As an extended example, we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use this model to extend the circuit language with some recursive types.

The Beta-Bernoulli process and algebraic effects

Sam Staton, Dario Stein, Hongseok Yang +3 more

cs.PL · · cited 23× · arXiv ↗ · more like this ·

In this paper we use the framework of algebraic effects from programming language theory to analyze the Beta-Bernoulli process, a standard building block in Bayesian models. Our analysis reveals the importance of abstract data types, and two types of program equations, called commutativity and discardability. We develop an equational theory of terms that use the Beta-Bernoulli process, and show that the theory is complete with respect to the measure-theoretic semantics, and also in the syntactic sense of Post. Our analysis has a potential for being generalized to other stochastic processes relevant to Bayesian modelling, yielding new understanding of these processes from the perspective of programming.

Transition systems over games

Paul Blain Levy, Sam Staton

Artificial Intelligence · University of Birmingham Research Portal (University of Birmingham) · · cited 23× · DOI ↗ · more like this ·

We describe a framework for game semantics combining operational and denotational accounts. A game is a bipartite graph of "passive" and "active" positions, or a categorical variant with morphisms between positions.

Universal Properties in Quantum Theory

Mathieu Huot, Sam Staton

quant-ph · · cited 22× · arXiv ↗ · more like this ·

We argue that notions in quantum theory should have universal properties in the sense of category theory. We consider the completely positive trace preserving (CPTP) maps, the basic notion of quantum channel. Physically, quantum channels are derived from pure quantum theory by allowing discarding. We phrase this in category theoretic terms by showing that the category of CPTP maps is the universal monoidal category with a terminal unit that has a functor from the category of isometries. In other words, the CPTP maps are the affine reflection of the isometries.

A monad for full ground reference cells

Ohad Kammar, Paul B. Levy, Sean K. Moss +1 more

cs.PL · · cited 22× · arXiv ↗ · more like this ·

We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.

Instances of Computational Effects: An Algebraic Perspective

Sam Staton

Artificial Intelligence · Logic in Computer Science · · cited 21× · DOI ↗ · more like this ·

Abstract—We investigate the connections between computational effects, algebraic theories, and monads on functor categories. We develop a syntactic framework with variable binding that allows us to describe equations between programs while taking into account the idea that there may be different instances of a particular computational effect. We use our framework to give a general account of several notions of computation that had previously been analyzed in terms of monads on presheaf categories: the analysis of local store by Plotkin and Power; the analysis of restriction by Pitts; and the analysis of the pi calculus by Stark. I.

General Structural Operational Semantics through Categorical Logic

Sam Staton

Artificial Intelligence · Proceedings - Symposium on Logic in Computer Science · · cited 20× · DOI ↗ · more like this ·

Certain principles are fundamental to operational semantics, regardless of the languages or idioms involved. Such principles include rule-based definitions and proof techniques for congruence results. We formulate these principles in the general context of categorical logic. From this general formulation we recover precise results for particular language idioms by interpreting the logic in particular categories. For instance, results for first-order calculi, such as CCS, arise from considering the general results in the category of sets. Results for languages involving substitution and name generation, such as the pi-calculus, arise from considering the general results in categories of sheaves and group actions. As an extended example, we develop a tyft/tyxt-like rule format for open bisimulation in the pi-calculus.

A Monad for Probabilistic Point Processes

Swaraj Dash, Sam Staton

cs.PL · · cited 19× · arXiv ↗ · more like this ·

A point process on a space is a random bag of elements of that space. In this paper we explore programming with point processes in a monadic style. To this end we identify point processes on a space X with probability measures of bags of elements in X. We describe this view of point processes using the composition of the Giry and bag monads on the category of measurable spaces and functions and prove that this composition also forms a monad using a distributive law for monads. Finally, we define a morphism from a point process to its intensity measure, and show that this is a monad morphism. A special case of this monad morphism gives us Wald's Lemma, an identity used to calculate the expected value of the sum of a random number of random variables. Using our monad we define a range of point processes and point process operations and compositionally compute their corresponding intensity…

Substitution, jumps, and algebraic effects

Marcelo Fiore, Sam Staton

Artificial Intelligence · Radboud Repository (Radboud University) · · cited 17× · DOI ↗ · more like this ·

Algebraic structures abound in programming languages. The starting point for this paper is the following theorem: (first-order) algebraic signatures can themselves be described as free algebras for a (second-order) algebraic theory of substitution. Transporting this to the realm of programming languages, we investigate a computational metalanguage based on the theory of substitution, demonstrating that substituting corresponds to jumping in an abstract machine. We use the theorem to give an interpretation of a programming language with arbitrary algebraic effects into the metalanguage with substitution/jumps.

Higher Order Automatic Differentiation of Higher Order Functions

Mathieu Huot, Sam Staton, Matthijs Vákár

cs.PL · · cited 16× · arXiv ↗ · more like this ·

We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher-order language with algebraic data types and we characterise it as the unique structure-preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming based on diffeological spaces. We show that it interprets our language and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is in essence a logical relations argument. Throughout we show how the analysis extends to AD methods for computing higher-order derivatives using a Taylor approximation.

Quantum channels as a categorical completion

Mathieu Huot, Sam Staton

cs.LO · · cited 16× · arXiv ↗ · more like this ·

We propose a categorical foundation for the connection between pure and mixed states in quantum information and quantum computation. The foundation is based on distributive monoidal categories. First, we prove that the category of all quantum channels is a canonical completion of the category of pure quantum operations (with ancilla preparations). More precisely, we prove that the category of completely positive trace-preserving maps between finite-dimensional C*-algebras is a canonical completion of the category of finite-dimensional vector spaces and isometries. Second, we extend our result to give a foundation to the topological relationships between quantum channels. We do this by generalizing our categorical foundation to the topologically-enriched setting. In particular, we show that the operator norm topology on quantum channels is the canonical topology induced by the norm…