LNL polycategories and doctrines of linear logic
From MaRDI portal
Publication:6135749
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.
Cites work
- scientific article; zbMATH DE number 2134022 (Why is no real title available?)
- scientific article; zbMATH DE number 1226952 (Why is no real title available?)
- scientific article; zbMATH DE number 575948 (Why is no real title available?)
- scientific article; zbMATH DE number 2079022 (Why is no real title available?)
- scientific article; zbMATH DE number 1512620 (Why is no real title available?)
- scientific article; zbMATH DE number 2172971 (Why is no real title available?)
- scientific article; zbMATH DE number 1860105 (Why is no real title available?)
- scientific article; zbMATH DE number 1405668 (Why is no real title available?)
- scientific article; zbMATH DE number 7204444 (Why is no real title available?)
- scientific article; zbMATH DE number 3316072 (Why is no real title available?)
- scientific article; zbMATH DE number 970691 (Why is no real title available?)
- ! and ? – Storage as tensorial strength
- *-Autonomous categories and linear logic
- *-autonomous categories. With an appendix by Po-Hsiang Chu
- A syntax for linear logic
- A unified framework for generalized multicategories
- Adjunction models for call-by-push-value with stacks
- An explicit formula for the free exponential modality of linear logic
- Bifibrations of polycategories and classical linear logic
- Braided skew monoidal categories
- Categorical homotopy theory
- Categorical semantics of linear logic
- Classical linear logic of implications
- Closed categories generated by commutative monads
- Closed categories vs. closed multicategories
- Coherence via focusing for symmetric skew monoidal categories
- Cyclic multicategories, multivariable adjunctions and mates
- Dwyer-Kan homotopy theory for cyclic operads
- Glueing and orthogonality for models of linear logic
- Higher cyclic operads
- Introduction to extensive and distributive categories
- Linear usage of state
- On the unity of logic
- Polycategories
- Polycategories via pseudo-distributive laws
- Premonoidal categories and notions of computation
- Proof theory in the abstract
- Representable multicategories
- Skew monoidal categories and skew multicategories
- Skew-monoidal categories and bialgebroids.
- Strong functors and monoidal monads
- Tensors, monads and actions
- The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions
- The enriched effect calculus: syntax and semantics
- The linear-non-linear substitution 2-monad
- The sequent calculus of skew monoidal categories
- Weakly distributive categories
Cited in
(2)
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)
