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

Abstract

In this paper, we present a typed lambda calculus ${\bf SILL}(\lambda)_{\Sigma}$, 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 $\Sigma$. We introduce the concept of a $\Sigma$-assemblage to characterise models of ${\bf SILL}(\lambda)_{\Sigma}$ 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 $\Sigma$-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 $\Sigma$-assemblages and show that the 2-category of $\Sigma$-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.