A Nominal Approach to Probabilistic Separation Logic

Reference. A Nominal Approach to Probabilistic Separation Logic

Cite

Cite as @li-2024-a (helia, typst) · \cite{li-2024-a} (LaTeX)

BibTeX

bibtex · 1 line

@inproceedings{li-2024-a, series={LICS ’24}, title={A Nominal Approach to Probabilistic Separation Logic}, url={http://dx.doi.org/10.1145/3661814.3662135}, DOI={10.1145/3661814.3662135}, booktitle={Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science}, publisher={ACM}, author={Li, John M. and Aytac, Jon and Johnson-Freyd, Philip and Ahmed, Amal and Holtzen, Steven}, year={2024}, month=July, pages={1–14}, collection={LICS ’24} }

hayagriva YAML (typst)

yaml · 17 lines

li-2024-a:
  type: article
  title: A Nominal Approach to Probabilistic Separation Logic
  author:
  - Li, John
  - Aytac, Jon
  - Johnson-Freyd, Philip
  - Ahmed, Amal
  - Holtzen, Steven
  date: 2024-07
  page-range: 1-14
  serial-number:
    doi: 10.1145/3661814.3662135
  parent:
    type: proceedings
    title: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science
    publisher: ACM

Download: li-2024-a.bib · li-2024-a.yml

Cited by (1)

Categorical Semantics of Probabilistic Symbolic Execution li-2026-categoricalPLDI · 2026

Symbolic execution has emerged as a powerful technique for scaling exact probabilistic inference to languages with more expressive features. But, this expressivity comes at a price: probabilistic programming languages based on symbolic execution are difficult to debug, optimize, and prove correct due to the many intricacies inherent to high-performance symbolic execution strategies. We aim to make it easier to work with probabilistic symbolic executors by developing symbolic sets , a new semantic domain that cleanly captures the notion of computation underlying symbolic execution. Just as a symbolic executor replaces ordinary execution with a lifted semantics, symbolic set theory replaces ordinary set theory with a lifted mathematics : the category of symbolic sets is a Grothendieck topos, which allows type theory to be used as a metalanguage for working with symbolic sets and functions. We prove a metatheorem that shows how a large class of definitional interpreters written in the internal language of symbolic sets are automatically correct for their ordinary set-theoretic interpretations. Using this metatheorem, we give the first full correctness argument for a symbolic probabilistic language with higher-order functions, type-directed state merging, pattern matching, and structural recursion.

PDF · DOI · pldb

Cites 52 works (7 here)

With notes (7)

Lilac: A Modal Separation Logic for Conditional Probability li-2023-lilacPLDI · 2023

We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. Inspired by an analogy with mutable state where sampling corresponds to dynamic allocation, we show how probability spaces over a fixed, ambient sample space appear to be the natural analogue of heap fragments, and present a new combining operation on them such that probability spaces behave like heaps and measurability of random variables behaves like ownership. This combining operation forms the basis for our model of separation, and produces a logic with many pleasant properties. In particular, Lilac has a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs. Then we propose a new modality based on disintegration theory for reasoning about conditional probability. We show how the resulting modal logic validates examples from prior work, and give a formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.

PDF · DOI · arXiv · pldb

A domain theory for statistical probabilistic programming vakar-2019-aPOPL · 2019

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 higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore’s axiomatic domain theory and a model of Kock’s synthetic measure theory.

PDF · DOI · pldb

A convenient category for higher-order probability theory heunen-2017-aLICS · 2017

DOI · arXiv

Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints staton-2016-semanticsLICS · 2016

DOI · arXiv

Nominal Sets: Names and Symmetry in Computer Science pitts_nominal_sets2013

On the Logic of Bunched Implications — and its relation to separation logic biering_bunched_20042004

Web

Separation logic: A logic for shared mutable data structures reynolds_separation_2002LICS · 2002

In joint work with Peter O’Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a “separating conjunction” that asserts that its subformulas hold for disjoint parts of the heap, and a closely related “separating implication”. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.

DOI

External (45)

Equivalence and Conditional Independence in Atomic Sheaf Logic (2024)
A separation logic for negative dependence (2022)
Higher-order probabilistic adversarial computations: categorical semantics and program logics (2021)
A Quantum Interpretation of Bunched Logic & Quantum Separation Logic (2021)
A Bunched Logic for Conditional Independence (2020)
Gelfand-type duality for commutative von Neumann algebras (2020)
Probabilistic programming semantics for name generation (2020)
Measure, integration & real analysis (2020)
A synthetic approach to Markov kernels, conditional independence, and theorems on sufficient statistics (2019)
A probabilistic separation logic (2019)
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization (2018)
Synthetic Probability Theory (2018)
Denotational validation of higher-order Bayesian inference (2017)
Convolution as a Unifying Concept (2016)
Revétements Étales et Groupe Fondamental (SGA 1) (2016)
254A, notes 0: A review of probability theory (2015)
Topological Galois Theory (2013)
Name-passing process calculi: operational models and structural operational semantics (2007)
Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July (2006)
Categorical Aspects of Topology and Analysis: Proceedings of an International Conference Held at Carleton University (2006)
The semantics of BI and resource tableaux (2005)
About N-quantifiers (2003)
Nominal logic, a first order theory of names and binding (2003)
Localic Galois theory (2000)
On the Galois theory of Grothendieck (2000)
Semi-pullbacks and bisimulation in categories of Markov processes (1999)
Change of base for measure spaces (1998)
Conditioning as disintegration (1997)
Representing topoi by topological groupoids (1996)
Syntactic control of interference revisited (1995)
A functional theory of local names (1994)
A model for syntactic control of interference (1993)
Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new? (1993)
Sheaves in geometry and logic: A first introduction to topos theory (1992)
Freyd's models for the independence of the axiom of choice (1989)
An extension of the Galois theory of Grothendieck (1984)
The lambda calculus (1984)
Boolean classifying topoi (1983)
Full continuous embeddings of toposes (1982)
Syntactic control of interference (1978)
On closed categories of functors (1970)
On the fundamental ideas of measure theory (1949)
A sheaf theoretic approach to measure theory. Ph. D. Dissertation
Foundations of modern probability
10.4230/lipics.calco.2017.1