Michael Shulman - LNL polycategories and doctrines of linear logic

lmcs:7662 - Logical Methods in Computer Science, April 5, 2023, Volume 19, Issue 2 - https://doi.org/10.46298/lmcs-19(2:1)2023
LNL polycategories and doctrines of linear logicArticle

Authors: Michael Shulman

    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.


    Volume: Volume 19, Issue 2
    Published on: April 5, 2023
    Accepted on: February 16, 2023
    Submitted on: July 10, 2021
    Keywords: Mathematics - Category Theory,Computer Science - Logic in Computer Science

    Classifications

    Mathematics Subject Classification 20201

    Consultation statistics

    This page has been seen 2112 times.
    This article's PDF has been downloaded 464 times.