Reference. Glueing and orthogonality for models of linear logic

Martin Hyland, Andrea Schalk · TCS · 2003 · linear-logic · DOI
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.

Cite
Cite as @hyland_glueing_2003 (helia, typst) · \cite{hyland_glueing_2003} (LaTeX)
BibTeX
bibtex · 16 lines
@article{hyland_glueing_2003,
 title = {Glueing and orthogonality for models of linear logic},
 author = {Hyland, Martin and Schalk, Andrea},
 year = {2003},
 doi = {10.1016/S0304-3975(01)00241-9},
 url = {https://linkinghub.elsevier.com/retrieve/pii/S0304397501002419},
 urldate = {2024-03-04},
 journal = {Theoretical Computer Science},
 volume = {294},
 number = {1-2},
 pages = {183--231},
 month = {February},
 language = {en},
 abstract = {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.},
 issn = {03043975}
}
hayagriva YAML (typst)
yaml · 20 lines
hyland_glueing_2003:
  type: article
  title: Glueing and orthogonality for models of linear logic
  author:
  - Hyland, Martin
  - Schalk, Andrea
  date: 2003-02
  page-range: 183-231
  url:
    value: https://linkinghub.elsevier.com/retrieve/pii/S0304397501002419
    date: 2024-03-04
  serial-number:
    doi: 10.1016/S0304-3975(01)00241-9
    issn: '03043975'
  abstract: '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.'
  parent:
    type: periodical
    title: Theoretical Computer Science
    issue: 1–2
    volume: 294
Download: hyland_glueing_2003.bib · hyland_glueing_2003.yml
Cited by (8)

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 𝜆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.
Web

Stabilized profunctors and stable species of structures fiore-2024-stabilizedLMCS · 2024
We introduce a bicategorical model of linear logic which is a novel variation of the bicategory of groupoids, profunctors, and natural transformations. Our model is obtained by endowing groupoids with additional structure, called a kit, to stabilize the profunctors by controlling the freeness of the groupoid action on profunctor elements. The theory of generalized species of structures, based on profunctors, is refined to a new theory of stable species of structures between groupoids with Boolean kits. Generalized species are in correspondence with analytic functors between presheaf categories; in our refined model, stable species are shown to be in correspondence with restrictions of analytic functors, which we characterize as being stable, to full subcategories of stabilized presheaves. Our motivating example is the class of finitary polynomial functors between categories of indexed sets, also known as normal functors, that arises from kits enforcing free actions. We show that the bicategory of groupoids with Boolean kits, stable species, and natural transformations is cartesian closed. This makes essential use of the logical structure of Boolean kits and explains the well-known failure of cartesian closure for the bicategory of finitary polynomial functors between categories of set-indexed families and cartesian natural transformations. The paper additionally develops the model of classical linear logic underlying the cartesian closed structure and clarifies the connection to stable domain theory.
DOI · arXiv

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

Fixpoint constructions in focused orthogonality models of linear logic fiore-2023-fixpointMFPS · 2023
Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to establish termination properties in classical formal systems. It was given a general treatment with the concept of orthogonality category, of which numerous models of linear logic are instances, by Hyland and Schalk. This paper considers the subclass of focused orthogonalities. We develop a theory of fixpoint constructions in focused orthogonality categories. Central results are lifting theorems for initial algebras and final coalgebras. These crucially hinge on the insight that focused orthogonality categories are relational fibrations. The theory provides an axiomatic categorical framework for models of linear logic with least and greatest fixpoints of types. We further investigate domain-theoretic settings, showing how to lift bifree algebras, used to solve mixed-variance recursive type equations, to focused orthogonality categories.
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

Free Commutative Monoids in Homotopy Type Theory choudhury-2023-freeMFPS · 2023
We develop a constructive theory of finite multisets in Homotopy Type Theory, defining them as free commutative monoids. After recalling basic structural properties of the free commutative-monoid construction, we formalise and establish the categorical universal property of two, necessarily equivalent, algebraic presentations of free commutative monoids using 1-HITs. These presentations correspond to two different equational theories invariably including commutation axioms. In this setting, we prove important structural combinatorial properties of finite multisets. These properties are established in full generality without assuming decidable equality on the carrier set. As an application, we present a constructive formalisation of the relational model of classical linear logic and its differential structure. This leads to constructively establishing that free commutative monoids are conical refinement monoids. Thereon we obtain a characterisation of the equality type of finite multisets and a new presentation of the free commutative-monoid construction as a set-quotient of the list construction. These developments crucially rely on the commutation relation of creation/annihilation operators associated with the free commutative-monoid construction seen as a combinatorial Fock space.
DOI · arXiv

A Combinatorial Approach to Higher-Order Structure for Polynomial Functors fiore-2022-aFSCD · 2022
Polynomial functors are categorical structures used in a variety of applications across theoretical computer science; for instance, in database theory, denotational semantics, functional programming, and type theory. A well-known problem is that the bicategory of finitary polynomial functors between categories of indexed sets is not cartesian closed, despite its success and influence on denotational models and linear logic. This paper introduces a formal bridge between the model of finitary polynomial functors and the combinatorial theory of generalised species of structures. Our approach consists in viewing finitary polynomial functors as free analytic functors, which correspond to free generalised species. In order to systematically consider finitary polynomial functors from this combinatorial perspective, we study a model of groupoids with additional logical structure; this is used to constrain the generalised species between them. The result is a new cartesian closed bicategory that embeds finitary polynomial functors.
DOI

*-Autonomous Envelopes and Conservativity shulman-2021-autonomousEPTCS · 2021
DOI · arXiv
Cites 50 works (3 here)
With notes (3)

Two-dimensional monad theory blackwell_kelly_power_1989JPAA · 1989
Web

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

Categories for the Working Mathematician maclane_19711971
Web
External (47)
hyland_glueing_2003 reference entries/refs/hyland_glueing_2003/hyland_glueing_2003.hel