Reference. Linear Effects, Exceptions, and Resource Safety: A Curry-Howard Correspondence for Destructors

Sidney Congard, Guillaume Munch-Maccagnoni, Rémi Douence · ESOP · 2026 · linear-logic effects · PDF · DOI · arXiv · pldb
We analyse the problem of combining linearity, effects, and exceptions, in abstract models of programming languages, as the issue of providing some kind of strength for a monad 𝑇(−⊕𝐸) in a linear setting. We consider in particular for T the allocation monad, which we introduce to model and study resource-safety properties. We apply these results to a series of two linear effectful calculi for which we establish their resource-safety properties. The first calculus is a linear (optionally ordered) call-by-push-value language with two allocation effects 𝐧𝐞𝐰 and 𝐝𝐞𝐥𝐞𝐭𝐞. The resource-safety properties follow from the linear and ordered character of the typing rules. We then integrate exceptions with linearity and effects by adjoining default destruction actions to types, as inspired by C++/Rust destructors. We see destructors as objects 𝛿:𝐴→𝑇𝐼 in the slice category over 𝑇𝐼. This construction gives rise to a second calculus, the resource call-by-push-value, featuring exceptions and destructors, and whose weakening and exchange rules perform side-effects. It is therefore affine at the level of types but ordered at the level of derivations. As in C++ and Rust, a “move” operation—the side-effecting exchange rule—is necessary for releasing resources in random order, as opposed to LIFO order.

Cite
Cite as @congard-2026-linear (helia, typst) · \cite{congard-2026-linear} (LaTeX)
BibTeX
bibtex · 1 line
@inbook{congard-2026-linear, title={Linear Effects, Exceptions, and Resource Safety: A Curry-Howard Correspondence for Destructors}, ISBN={9783032227201}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-032-22720-1_8}, DOI={10.1007/978-3-032-22720-1_8}, booktitle={Programming Languages and Systems}, publisher={Springer Nature Switzerland}, author={Congard, Sidney and Munch-Maccagnoni, Guillaume and Douence, Rémi}, year={2026}, pages={190–219} }
hayagriva YAML (typst)
yaml · 18 lines
congard-2026-linear:
  type: chapter
  title: 'Linear Effects, Exceptions, and Resource Safety: A Curry-Howard Correspondence for Destructors'
  author:
  - Congard, Sidney
  - Munch-Maccagnoni, Guillaume
  - Douence, Rémi
  date: 2026
  page-range: 190-219
  url: http://dx.doi.org/10.1007/978-3-032-22720-1_8
  serial-number:
    doi: 10.1007/978-3-032-22720-1_8
    isbn: '9783032227201'
    issn: 1611-3349
  parent:
    type: book
    title: Programming Languages and Systems
    publisher: Springer Nature Switzerland
Download: congard-2026-linear.bib · congard-2026-linear.yml
Cites 58 works (3 here)
With notes (3)

Resource Polymorphism munchmaccagnoni-2018-resourcearXiv · 2018
We present a resource-management model for ML-style programming languages, designed to be compatible with the OCaml philosophy and runtime model. This is a proposal to extend the OCaml language with destructors, move semantics, and resource polymorphism, to improve its safety, efficiency, interoperability, and expressiveness. It builds on the ownership-and-borrowing models of systems programming languages (Cyclone, C++11, Rust) and on linear types in functional programming (Linear Lisp, Clean, Alms). It continues a synthesis of resources from systems programming and resources in linear logic initiated by Baker. It is a combination of many known and some new ideas. On the novel side, it highlights the good mathematical structure of Stroustrup’s “Resource acquisition is initialisation” (RAII) idiom for resource management based on destructors, a notion sometimes confused with finalizers, and builds on it a notion of resource polymorphism, inspired by polarisation in proof theory, that mixes C++‘s RAII and a tracing garbage collector (GC). The proposal targets a new spot in the design space, with an automatic and predictable resource-management model, at the same time based on lightweight and expressive language abstractions. It is backwards-compatible: current code is expected to run with the same performance, the new abstractions fully combine with the current ones, and it supports a resource-polymorphic extension of libraries. It does so with only a few additions to the runtime, and it integrates with the current GC implementation. It is also compatible with the upcoming multicore extension, and suggests that the Rust model for eliminating data-races applies. Interesting questions arise for a safe and practical type system, many of which have already been thoroughly investigated in the languages and prototypes Cyclone, Rust, and Alms.
arXiv

A theory of effects and resources: adjunction models and polarised calculi curien-2016-aPOPL · 2016
DOI · pldb

Linear logic girard_linear_1987TCS · 1987
The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
DOI
External (55)
congard-2026-linear reference entries/refs/congard-2026-linear/congard-2026-linear.hel