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

Daniel Rogozin

In this paper, we present a typed lambda calculus $\mathbf{SILL}(\lambda {)}_{\Sigma }$, a type-theoretic version of multiplicative intuitionistic linear logic with subexponentials, that is, we have m…