Reference. Syntax and semantics of focalisation with relative monads and comonads

The logical principles of focalisation and polarisation can be used to design well-behaved term syntaxes for sequent calculus, which play a role as meta-languages for describing effectful computation. On the semantics side, this corresponds to an axiomatic and polarised notion of model of computation stated in terms of adjunctions over non-associative categories. In this paper, we study the special and delicate cases of resource and effect modalities in a general intuitionistic and linear setting: an exponential comonad ! (refining □) and a strong monad ◊. The starting point of our contribution is noticing that the completeness for a polarised syntax for ! and ◊ with respect to (co)monads in linear call-by-push-value models can be achieved if we move to relative (co)monads: more precisely, comonads relative to ↓ (the positive shift functor) for ! and monads relative to ↑ (the negative shift functor) for ◊. These specialisations of the concept of relative (co)monad to call-by-push-value adjunctions recently appeared. Yet the syntax we present arose from proof-theoretic consideration, without the link with relative (co)monads being noticed at the time. Our first remark is thus that (co)monads relative to a call-by-push-value adjunction have been motivated previously from a proof-theoretic perspective in the context of focalisation, which also provides a meta-language for these concepts in an effectful setting. We carry out the study of these modalities from the axiomatic, non-associative point of view. We recall the notion of adjunction over non-associative categories, and establish correspondence results between this notion of adjunction and that of relative adjunction. This correspondence is then extended to linear-non-linear and strong versions of adjunctions as needed to model ! and ◊.

Cite

Cite as @mangel-2026-syntax (helia, typst) · \cite{mangel-2026-syntax} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{mangel-2026-syntax,
  author = {Éléonore Mangel and Paul-André Melliès and Guillaume Munch-Maccagnoni},
  title = {Syntax and semantics of focalisation with relative monads and comonads},
  year = {2026},
  month = {6},
  eprint = {2606.14652},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 10 lines
mangel-2026-syntax:
  type: misc
  title: Syntax and semantics of focalisation with relative monads and comonads
  author:
  - Mangel, Éléonore
  - Melliès, Paul-André
  - Munch-Maccagnoni, Guillaume
  date: 2026-06
  serial-number:
    arxiv: '2606.14652'
Cites 53 works (8 here)
With notes (8)

Classical Notions of Computation and the Hasegawa-Thielecke Theorem mangel-2026-classical

In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus, the linear classical L -calculus. A main challenge in designing a denotational semantics for the calculus is to accommodate both call-by-value and call-by-name evaluation strategies, which leads to a failure of associativity of composition. In order to tackle this issue, we define a notion of adjunction between graph morphisms on non-associative categories, which we use to formulate polarized and non-associative notions of symmetric monoidal closed duploid and of dialogue duploid. We show that they provide a direct style counterpart to adjunction models: linear effect adjunctions for the (linear) call-by-push-value calculus and dialogue chiralities for linear continuations, respectively. In particular, we show that the syntax of the linear classical L -calculus can be interpreted in any dialogue duploid, and that it defines in fact a syntactic dialogue duploid. As an application, we establish, by semantic as well as syntactic means, the Hasegawa-Thielecke theorem, which states that the notions of central map and of thunkable map coincide in any dialogue duploid (in particular, for any double negation monad on a symmetric monoidal category).
PDF · DOI · arXiv · pldb

Notions of Stack-manipulating Computation and Relative Monads jiang_xue_new_2025

Monads provide a simple and concise interface to user-defined computational effects in functional programming languages. This enables equational reasoning about effects, abstraction over monadic interfaces and the development of monad transformer stacks to allow for multiple effects. Compiler implementors and assembly code programmers similarly virtualize effects, and would benefit from similar abstractions if possible. However, the implementation details of effects seem disconnected from the high-level monad interface: at this lower level much of the design is in the layout of the runtime stack, which is not accessible in a high-level programming language.

We demonstrate that the monadic interface can be faithfully adapted from high-level functional programming to a lower level setting with explicit stack manipulation. We use a polymorphic call-by-push-value (CBPV) calculus as a setting that captures the essence of stack-manipulation, with a type system that allows programs to define domain-specific stack structures. Within this setting, we show that the existing category-theoretic notion of a relative monad can be used to model the stack-based implementation of computational effects. To demonstrate generality, we adapt a variety of standard monads to relative monads. Additionally, we show that stack-manipulating programs can benefit from a generalization of do-notation we call “monadic blocks” that allow all CBPV code to be reinterpreted to work with an arbitrary relative monad. As an application, we show that all relative monads extend automatically to relative monad transformers, a process which is not automatic for monads in pure languages.

PDF · DOI · pldb

A theory of effects and resources: adjunction models and polarised calculi curien-2016-a

DOI · pldb

Models of a Non-associative Composition munchmaccagnoni-2014-models

DOI

Focalisation and Classical Realisability munchmaccagnoni-2009-focalisation

DOI

Call-By-Push-Value: A Functional/Imperative Synthesis levy-2003-callbypushvalue

DOI

A mixed linear and non-linear logic: Proofs, terms and models: Extended abstract bentonMixedLinearNonlinear1995

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

Linear logic girard_linear_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 (45)
mangel-2026-syntax reference entries/refs/mangel-2026-syntax/mangel-2026-syntax.hel