LNL polycategories and doctrines of linear logic

DOI10.46298/LMCS-19(2:1)2023arXiv2106.15042MaRDI QIDQ6135749FDOQ6135749

Authors: Michael Shulman 

Publication date: 26 August 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/2106.15042

zbMATH Keywords

linear logicmulticategorysequent calculuspolycategorydoctrineexponential modality

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Categorical semantics of linear logic
• Title not available (Why is that?)
• Premonoidal categories and notions of computation
• Title not available (Why is that?)
• Weakly distributive categories
• Polycategories
• Dwyer-Kan homotopy theory for cyclic operads
• Title not available (Why is that?)
• Introduction to extensive and distributive categories
• Representable multicategories
• Title not available (Why is that?)
• Strong functors and monoidal monads
• Skew monoidal categories and skew multicategories
• Skew-monoidal categories and bialgebroids.
• *-autonomous categories. With an appendix by Po-Hsiang Chu
• Title not available (Why is that?)
• Categorical homotopy theory
• Title not available (Why is that?)
• On the unity of logic
• Title not available (Why is that?)
• Closed categories generated by commutative monads
• Glueing and orthogonality for models of linear logic
• Polycategories via pseudo-distributive laws
• A unified framework for generalized multicategories
• *-Autonomous categories and linear logic
• Title not available (Why is that?)
• ! and ? – Storage as tensorial strength
• The sequent calculus of skew monoidal categories
• Tensors, monads and actions
• Braided skew monoidal categories
• An explicit formula for the free exponential modality of linear logic
• Adjunction models for call-by-push-value with stacks
• Proof theory in the abstract
• A syntax for linear logic
• Closed categories vs. closed multicategories
• Linear usage of state
• Higher cyclic operads
• Classical linear logic of implications
• Cyclic multicategories, multivariable adjunctions and mates
• Title not available (Why is that?)
• The linear-non-linear substitution 2-monad
• Bifibrations of polycategories and classical linear logic
• The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions
• Coherence via focusing for symmetric skew monoidal categories
• The enriched effect calculus: syntax and semantics

Cited In (2)

• Title not available (Why is that?)
• Clones, closed categories, and combinatory logic

This page was built for publication: LNL polycategories and doctrines of linear logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135749)