Reference. Stabilized profunctors and stable species of structures
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.
Cite
Cited by (1)
Modular abstract syntax trees (MAST): substitution tensors with second-class sorts fiore-2025-modular
We adapt Fiore, Plotkin, and Turi’s treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value lambda-calculus (CBV) and Levy’s Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appearing in variable contexts changes the characterisation of the abstract syntax from monoids in monoidal categories to actions in actegories. We reproduce much of the development through bicategorical arguments. We apply the resulting theory by proving substitution lemmata for varieties of CBV.
Cites 51 works (4 here)
With notes (4)
A Combinatorial Approach to Higher-Order Structure for Polynomial Functors fiore-2022-a
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.
Indexed containers altenkirch_indexed_2015
We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide normal forms for strictly positive families in much the same way that containers provide normal forms for strictly positive types. Interestingly, this step from containers to indexed containers is achieved without having to extend the core type theory. Most of the construction presented here has been formalized using the Agda system.
Glueing and orthogonality for models of linear logic hyland_glueing_2003
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.
Linear logic girard_linear_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.
External (47)
- Intersection Type Distributors (2021)
- A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory (2021)
- Infinity-Operads as Analytic Monads (2021)
- On Diers theory of Spectrum I: Stable functors and right multi-adjoints (2020)
- Higher-Order Distributions for Differential Linear Logic (2019)
- Species, Profunctors and Taylor Expansion Weighted by SMCC (2018)
- A Logical Account for Linear Partial Differential Equations (2018)
- An introduction to differential linear logic: proof-nets, models and antiderivatives (2017)
- Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures (2017)
- Shapely monads and analytic functors (2017)
- Generalised species of rigid resource terms (2017)
- Compact Closed Bicategories (2016)
- Analytic functors between presheaf categories over groupoids (2014)
- Polynomial functors and polynomial monads (2012)
- Data Types with Symmetries and Polynomial Functors over Groupoids (2012)
- Probabilistic coherence spaces as a model of higher-order probabilistic computation (2011)
- Higher-Order Containers (2010)
- The cartesian closed bicategory of generalised species of structures (2007)
- Familial 2-functors and parametric right adjoints (2007)
- Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic (2007)
- Containers: Constructing strictly positive types (2005)
- Finiteness spaces (2005)
- Mathematical Models of Computational and Combinatorial Structures (2005)
- Generic morphisms, parametric representationsand weakly cartesian monads (2004)
- The differential lambda-calculus (2003)
- Two applications of analytic functors (2002)
- Distributors at work (lecture notes by T. Streicher) (2000)
- The trace factorisation of stable functors (1998)
- Combinatorial Species and Tree-like Structures (1997)
- Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories (1997)
- Connected limits, familial representability and Artin glueing (1995)
- Linear logic, totality and full completeness (1994)
- An algebraic approach to stable domains (1990)
- Quantitative domains, groupoids and linear logic (1989)
- Normal functors, power series and λ-calculus (1988)
- Combinatorial resolution of systems of differential equations (1988)
- Modelling polymorphism with categories (PhD thesis) (1988)
- The system F of variable types, fifteen years later (1986)
- Foncteurs analytiques et espèces de structures (1986)
- Une théorie combinatoire des séries formelles (1981)
- *-Autonomous Categories (LNM 752) (1979)
- Stable models of typed lambda-calculi (1978)
- Catégories localisables (PhD thesis) (1977)
- Data Types as Lattices (1976)
- Metric spaces, generalized logic, and closed categories (1973)
- Introduction to bicategories (1967)
- On ext and exact sequences (1961)