Term Assignment and Categorical Models for Intuitionistic Linear Logic with Subexponentials

In this paper, we present a typed lambda calculus SILL (λ) _Σ, a type-theoretic version of intuitionistic linear logic with subexponentials, that is, we have many resource comonadic modalities with some interconnections between them given by a subexponential signature. We also give proof normalisation rules and prove the strong normalisation and Church-Rosser properties for β-reduction by adapting the Tait-Girard method to subexponential modalities. Further, we analyse subexponentials from the point of view of categorical logic. We introduce the concepts of a Cocteau category and a Σ-assemblage to characterise models of linear type theories with a single exponential and affine and relevant subexponentials and a more general case respectively. We also generalise several known results from linear logic and show that every Cocteau category and a Σ-assemblage can be viewed as a symmetric monoidal closed category equipped with a family of monoidal adjunctions of a particular kind. In the final section, we give a stronger 2-categorical characterisation of Cocteau categories.