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

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

Nick Benton · CSL · 1995 · linear-logic · DOI

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.

Cite

Cite as @bentonMixedLinearNonlinear1995 (helia, typst) · \cite{bentonMixedLinearNonlinear1995} (LaTeX)

BibTeX

bibtex · 19 lines

@incollection{bentonMixedLinearNonlinear1995,
 title = {A mixed linear and non-linear logic: {Proofs}, terms and models: {Extended} abstract},
 author = {Benton, P. N.},
 year = {1995},
 isbn = {978-3-540-60017-6 978-3-540-49404-1},
 doi = {10.1007/BFb0022251},
 url = {http://link.springer.com/10.1007/BFb0022251},
 urldate = {2024-04-27},
 booktitle = {Computer {Science} {Logic}},
 editor = {Goos, Gerhard and Hartmanis, Juris and Van Leeuwen, Jan and Pacholski, Leszek and Tiuryn, Jerzy},
 volume = {933},
 pages = {121--135},
 publisher = {Springer Berlin Heidelberg},
 address = {Berlin, Heidelberg},
 note = {Series Title: Lecture Notes in Computer Science},
 language = {en},
 abstract = {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.},
 shorttitle = {A mixed linear and non-linear logic}
}

hayagriva YAML (typst)

yaml · 29 lines

bentonMixedLinearNonlinear1995:
  type: anthos
  title:
    value: 'A mixed linear and non-linear logic: {Proofs}, terms and models: {Extended} abstract'
    short: A mixed linear and non-linear logic
  author: Benton, P. N.
  date: 1995
  editor:
  - Goos, Gerhard
  - Hartmanis, Juris
  - Van Leeuwen, Jan
  - Pacholski, Leszek
  - Tiuryn, Jerzy
  page-range: 121-135
  url:
    value: http://link.springer.com/10.1007/BFb0022251
    date: 2024-04-27
  serial-number:
    doi: 10.1007/BFb0022251
    isbn: 978-3-540-60017-6 978-3-540-49404-1
  note: 'Series Title: Lecture Notes in Computer Science'
  abstract: 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.
  parent:
    type: anthology
    title: Computer {Science} {Logic}
    publisher:
      name: Springer Berlin Heidelberg
      location: Berlin, Heidelberg
    volume: 933

Download: bentonMixedLinearNonlinear1995.bib · bentonMixedLinearNonlinear1995.yml

Cited by (21)

Syntax and semantics of focalisation with relative monads and comonads mangel-2026-syntaxarXiv · 2026

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

◊

arXiv

Impredicativity in Linear Dependent Type Theory speight-2026-impredicativityarXiv · 2026

We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.

arXiv

S4 modal sequent calculus as intermediate logic and intermediate language caspar-2026-s4arXiv · 2026

In this short paper, we advocate for the idea that continuation-based intermediate languages correspond to intermediate logics. The goal of intermediate languages is to serve as a basis for compiler intermediate representations, allowing to represent expressive program transformations for optimisation and compilation, while preserving the properties that make programs compilable efficiently in the first place, such as the “stackability” of continuations. Intermediate logics are logics between intuitionistic and classical logic in terms of provability. Second-class continuations used in CPS-based intermediate languages correspond to a classical modal logic S4 with the added restriction that implications may only return modal types. This indeed corresponds to an intermediate logic, owing to the Gödel-McKinsey-Tarski theorem which states the intuitionistic nature of the modal fragment of S4. We introduce a three-kinded polarised sequent calculus for S4, together with an operational machine model that separates a heap from a stack. With this model we study a stackability property for the modal fragment of S4.

arXiv

Ordered Adjoint Logic roshal-2026-orderedAutomated Reasoning · 2026

Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most formulations, ordered types are also linear, requiring each resource to be used exactly once. Prior work by Kanovich et al. has investigated calculi that relax this constraint through subexponentials within a linear ordered logic. We generalize their work by using adjoint modalities to combine logics with varying fine-grained structural properties, including weakening, left contraction, right contraction, left mobility, and right mobility. We show that the resulting sequent calculus admits cut elimination. We further provide a natural deduction formulation in which structural rules are implicit, and show that proof checking for this system is decidable. This makes it a suitable foundation for an expressive adjoint programming language or logical framework.

DOI

Canonical bidirectional typechecking mihejevs-2025-canonicalarXiv · 2025

We demonstrate that the checkable/synthesisable split in bidirectional typechecking coincides with existing dualities in polarised System L, also known as polarised

𝜇 \tilde{𝜇}

-calculus. Specifically, positive terms and negative coterms are checkable, and negative terms and positive coterms are synthesisable. This combines a standard formulation of bidirectional typechecking with Zeilberger’s ‘cocontextual’ variant. We extend this to ordinary ‘cartesian’ System L using Mc Bride’s co-de Bruijn formulation of scopes, and show that both can be combined in a linear-nonlinear style, where linear types are positive and cartesian types are negative. This yields a remarkable 3-way coincidence between the shifts of polarised System L, LNL calculi, and bidirectional calculi.

arXiv

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsersPLDI · 2025

We present Dependent Lambek Calculus (Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ ), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ , linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.

We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.

PDF · DOI · arXiv (extended version) · Source code · pldb

The Formal Theory of Monads, Univalently vanderweide-2025-thexLMCS · 2025

We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal to a bicategory, and prove that it is univalent. We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects. Finally, we relate monads and adjunctions in arbitrary bicategories. Our work is formalized in Coq using the UniMath library.

DOI

Separated and Shared Effects in Higher-Order Languages amorim_hsu_independent2025

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

𝜆_{INI}^{2}

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

𝜆_{INI}^{2}

uses a categorical gluing construction.

Web

Displayed Monoidal Categories for the Semantics of Linear Logic ahrens-2024-displayedCPP · 2024

PDF · DOI · pldb

Polynomial Time and Dependent Types atkey-2024-polynomialPOPL · 2024

We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann. Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs’ resource usage, and to theoretical use as a form of synthetic computational complexity theory .

PDF · DOI · arXiv · pldb

UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC kavvos-2023-underBSL · 2023

We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e., a small 2-category. The logic is extended to a lambda calculus, establishing a Curry–Howard correspondence.

DOI · arXiv

LNL polycategories and doctrines of linear logic shulman-2023-lnlLMCS · 2023

We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly distributive categories with storage, commutative and strong monads, CBPV-structures, models of polarized calculi, Freyd-categories, and skew multicategories, as well as ordinary cartesian, symmetric, and planar multicategories and monoidal categories, symmetric polycategories, and linearly distributive and *-autonomous categories. To study such classes of structures uniformly, we define a notion of LNL doctrine, such that each of these classes of structures can be identified with the algebras for some such doctrine. We show that free algebras for LNL doctrines can be presented by a sequent calculus, and that every morphism of doctrines induces an adjunction between their 2-categories of algebras.

DOI · arXiv

Data Layout from a Type-Theoretic Perspective deyoung-2023-dataENTCS · 2023

The specifics of data layout can be important for the efficiency of functional programs and interaction with external libraries. In this paper, we develop a type-theoretic approach to data layout that could be used as a typed intermediate language in a compiler or to give a programmer more control. Our starting point is a computational interpretation of the semi-axiomatic sequent calculus for intuitionistic logic that defines abstract notions of cells and addresses. We refine this semantics so addresses have more structure to reflect possible alternative layouts without fundamentally departing from intuitionistic logic. We then add recursive types and explore example programs and properties of the resulting language.

DOI · arXiv

A two-level linear dependent type theory fu2023twolevellineardependenttypearXiv · 2023

We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system to assume tight resource bounds. A natural notion of irrelevancy is established where all proofs and types occurring inside programs are fully erasable without compromising their operational behavior. Through a heap-based operational semantics, we show that extracted programs always make computational progress and run memory clean. Additionally, programs can be freely reflected into the logical level for conducting deep proofs in the style of standard dependent type theories. This enables one to write resource safe programs and verify their correctness using a unified language.

Web · arXiv

Relating Message Passing and Shared Memory, Proof-Theoretically pfenning-2023-relatingCoordination Models and Languages · 2023

DOI

A Framework for Substructural Type Systems wood-2022-aESOP · 2022

Mechanisation of programming language research is of growing interest, and the act of mechanising type systems and their metatheory is generally becoming easier as new techniques are invented. However, state-of-the-art techniques mostly rely on structurality of the type system — that weakening, contraction, and exchange are admissible and variables can be used unrestrictedly once assumed. Linear logic, and many related subsequent systems, provide motivations for breaking some of these assumptions. We present a framework for mechanising the metatheory of certain substructural type systems, in a style resembling mechanised metatheory of structural type systems. The framework covers a wide range of simply typed syntaxes with semiring usage annotations, via a metasyntax of typing rules. The metasyntax for the premises of a typing rule is related to bunched logic, featuring both sharing and separating conjunction, roughly corresponding to the additive and multiplicative features of linear logic. We use the uniformity of syntaxes to derive type system-generic renaming, substitution, and a form of linearity checking.

PDF · DOI · pldb

Adjoint Reactive GUI Programming graulund-2021-adjointFoSSaCS · 2021

Most interaction with a computer is via graphical user interfaces. These are traditionally implemented imperatively, using shared mutable state and callbacks. This is efficient, but is also difficult to reason about and error prone. Functional Reactive Programming (FRP) provides an elegant alternative which allows GUIs to be designed in a declarative fashion. However, most FRP languages are synchronous and continually check for new data. This means that an FRP-style GUI will “wake up” on each program cycle. This is problematic for applications like text editors and browsers, where often nothing happens for extended periods of time, and we want the implementation to sleep until new data arrives. In this paper, we present an asynchronous FRP language for designing GUIs called

𝜆_{𝖶𝗂𝖽𝗀𝖾𝗍}

. Our language provides a novel semantics for widgets, the building block of GUIs, which offers both a natural Curry–Howard logical interpretation and an efficient implementation strategy.

DOI · arXiv

Fractional Types: Expressive and Safe Space Management for Ancilla Bits chen-2020-fractionalRC · 2020

DOI · arXiv

Syntax and Semantics of Quantitative Type Theory atkey-2018-syntaxLICS · 2018

DOI

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

DOI · pldb

Integrating Linear and Dependent Types krishnaswami_integrating_2015POPL · 2015

In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency.

PDF · DOI · pldb

Cites 15 works (2 here)

With notes (2)

Linear logic, *-autonomous categories and cofree coalgebras seely89Categories in computer science and logic (Boulder, CO, 1987) · 1989

DOI

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 (13)

Strong normalisation for the linear term calculus (1995)
A mixed linear and non-linear logic: Proofs, terms and models (preliminary report), Cambridge TR 352 (1994)
On intuitionistic linear logic (Bierman, Cambridge TR 346) (1994)
Conventional and uniqueness typing in graph rewrite systems (1993)
Linear λ-calculus and categorical models revisited (1993)
A term calculus for Intuitionistic Linear Logic (1993)
On the unity of logic (1993)
A taste of linear logic (1993)
Conventional and linear types in a logic of coalgebras (Jacobs, preprint) (1993)
Type theory and recursion (abstract) (Plotkin, LICS) (1993)
There's no substitute for linear logic (1992)
Operational aspects of linear lambda calculus (1992)
Notions of computation and monads (1991)