Intuitionistic Linear Logic with Subexponentials: Type Theory, Categorical Models and Realisability

Abstract

In this paper, we present a typed lambda calculus ${\bf SILL}(λ)_Σ$, a type-theoretic version of multiplicative intuitionistic linear logic with subexponentials, that is, we have many comonadic resource modalities with some interconnections between them given by a subexponential signature $Σ$. We introduce the concept of a $Σ$-assemblage to characterise models of ${\bf SILL}(λ)_Σ$ by expanding the concept of a linear category where one has multiple resource comonads and symmetric lax monoidal comonad morphisms. We also generalise several known results from linear logic and show that every $Σ$-assemblage can be viewed as a symmetric monoidal closed category equipped with a family of monoidal adjunctions and morphisms by modernising and generalising Benton's results by involving the formal theory of comonads in the fashion of Street. We give a stronger 2-categorical characterisation of $Σ$-assemblages and show that the 2-category of $Σ$-assemblages 1,2-fully faithfully embeds into the 2-category of particular families of monoidal adjunctions, their left morphisms and transformations, that is, polymodal expansions of linear-non-linear models. In the final section, we describe realisability models for the particular case of a three-element subexponential signature by describing BCI algebras with extra operators viewed as applicative morphisms and assemblies over them.