Reference. Separated and Shared Effects in Higher-Order Languages

Pedro H. Azevedo de Amorim, Justin Hsu · 2025 · effects separation-logic preprint · Web
Effectful programs interact in ways that go beyond simple input-output, making compositional reasoning challenging. Existing work has shown that when such programs are “separate”, i.e., when programs do not interfere with each other, it can be easier to reason about them. While reasoning about separated resources has been well-studied, there has been little work on reasoning about separated effects, especially for functional, higher-order programming languages. We propose two higher-order languages that can reason about sharing and separation in effectful programs. Our first language 𝜆INI has a linear type system and probabilistic semantics, where the two product types capture independent and possibly-dependent pairs. Our second language 𝜆INI2 is two-level, stratified language, inspired by Benton’s linear-non-linear (LNL) calculus. We motivate this language with a probabilistic model, but we also provide a general categorical semantics and exhibit a range of concrete models beyond probabilistic programming. We prove soundness theorems for all of our languages; our general soundness theorem for our categorical models of 𝜆INI2 uses a categorical gluing construction.

Cite
Cite as @amorim_hsu_independent (helia, typst) · \cite{amorim_hsu_independent} (LaTeX)
BibTeX
bibtex · 6 lines
@unpublished{amorim_hsu_independent,
 title = {Separated and Shared Effects in Higher-Order Languages},
 author = {Amorim, Pedro H. Azevedo de and Hsu, Justin},
 note = {Preprint},
 url = {https://pedrohaa.github.io/papers/independent.pdf}
}
hayagriva YAML (typst)
yaml · 8 lines
amorim_hsu_independent:
  type: manuscript
  title: Separated and Shared Effects in Higher-Order Languages
  author:
  - Amorim, Pedro H. Azevedo de
  - Hsu, Justin
  url: https://pedrohaa.github.io/papers/independent.pdf
  note: Preprint
Download: amorim_hsu_independent.bib · amorim_hsu_independent.yml
Cites 42 works (5 here)
With notes (5)

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 Higher-Order Language for Markov Kernels and Linear Operators amorim_2023_fossacsFoSSaCS · 2023

Much work has been done to give semantics to probabilistic programming languages. In recent years, most of the semantics used to reason about probabilistic programs fall in two categories: semantics based on Markov kernels and semantics based on linear operators.

Both styles of semantics have found numerous applications in reasoning about probabilistic programs, but they each have their strengths and weaknesses. Though it is believed that there is a connection between them there are no languages that can handle both styles of programming.

In this work we address these questions by defining a two-level calculus and its categorical semantics which makes it possible to program with both kinds of semantics. From the logical side of things we see this language as an alternative resource interpretation of linear logic, where the resource being kept track of is sampling instead of variable use.

DOI

Glueing and orthogonality for models of linear logic hyland_glueing_2003TCS · 2003
We present the general theory of the method of glueing and associated technique of orthogonality for constructing categorical models of all the structure of linear logic: in particular we treat the exponentials in detail. We indicate simple applications of the methods and show that they cover familiar examples.
DOI

The logic of bunched implications ohearn_pym_bi_1999BSL · 1999
We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI’s proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers [inline image] and [inline image] which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels.

A mixed linear and non-linear logic: Proofs, terms and models: Extended abstract bentonMixedLinearNonlinear1995CSL · 1995
Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad. This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.
DOI
External (37)
amorim_hsu_independent reference entries/refs/amorim_hsu_independent/amorim_hsu_independent.hel