Reference. Syntax and semantics of focalisation with relative monads and comonads
Cite
Cites 53 works (8 here)
With notes (8)
Classical Notions of Computation and the Hasegawa-Thielecke Theorem mangel-2026-classical
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.
A theory of effects and resources: adjunction models and polarised calculi curien-2016-a
Models of a Non-associative Composition munchmaccagnoni-2014-models
Focalisation and Classical Realisability munchmaccagnoni-2009-focalisation
Call-By-Push-Value: A Functional/Imperative Synthesis levy-2003-callbypushvalue
A mixed linear and non-linear logic: Proofs, terms and models: Extended abstract bentonMixedLinearNonlinear1995
Linear logic girard_linear_1987
External (45)
- A story of tensorial logic with two negations (2026)
- The Relative Monadic Metalanguage (2025)
- Recent advances in tensorial logic and functorial game semantics (2025)
- The formal theory of relative monads (2023)
- Note on Curry's style for linear call-by-push-value (2017)
- Game Semantics in String Diagrams (2012)
- Parametric monads and enriched adjunctions (2012)
- Linearising call-by-push-value (2011)
- Monads need not be endofunctors (2010)
- Resource modalities in tensor logic (2010)
- Focusing and polarization in linear, intuitionistic, and classical logics (2009)
- Enriching an Effect Calculus with Linear Types (2009)
- Realizability in classical logic (2009)
- Polarized and focalized linear and classical proofs (2005)
- C'est maintenant qu'on calcule, au cœur de la dualité (2005)
- A proof of the focalization property of linear logic (2004)
- Adjunction Models For Call-By-Push-Value With Stacks (2003)
- Polarized proof-nets and λμ-calculus (2003)
- A Proof Theoretical Account of Continuation Passing Style (2002)
- Completeness of continuation models for λμ-calculus (2002)
- Étude de la polarisation en logique (2002)
- Linearly used effects: monadic and CPS transformations into the linear lambda calculus (2002)
- Categorical and Kripke Semantics for Constructive S4 Modal Logic (2001)
- Control categories and duality: on the categorical semantics of the lambda-mu calculus (2001)
- The duality of computation (2000)
- The structure of call-by-value (2000)
- Constructive Classical Logic as CPS-Calculus (2000)
- Call-by-Push-Value: A Subsuming Paradigm (1999)
- Direct Models for the Computational Lambda Calculus (1999)
- Classical logic, continuation semantics and abstract machines (1998)
- Premonoidal categories and notions of computation (1997)
- A new deconstructive logic: linear logic (1997)
- Categorical Structure of Continuation Passing Style (1997)
- ! and ? – Storage as tensorial strength (1996)
- Linear logic, monads and the lambda calculus (1996)
- Axiomatic domain theory in categories of partial maps (1994)
- On the Unity of Logic (1993)
- Lambda-calculus, types and models (1993)
- Continuation Semantics or Expressing Implication by Negation (1993)
- A computational analysis of Girard's translation and LC (1992)
- Logic Programming with Focusing Proofs in Linear Logic (1992)
- Notions of Computation and Monads (1991)
- A new constructive logic: classic logic (1991)
- Computational lambda-calculus and monads (1989)
- Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur (1972)