Term Assignment and Categorical Models for Intuitionistic Linear Logic with Subexponentials

TL;DR

This paper introduces a typed lambda calculus for intuitionistic linear logic with subexponentials, proves normalization properties, and explores categorical models including Cocteau categories and Sigma-assemblages.

Contribution

It develops a type-theoretic framework for linear logic with subexponentials, proves key normalization results, and characterizes models categorically with new concepts like Cocteau categories.

Findings

Proved strong normalization and Church-Rosser properties for the calculus.

Introduced Cocteau categories and Sigma-assemblages as models.

Connected categorical logic with linear type theories.

Abstract

In this paper, we present a typed lambda calculus ${\bf SILL}(\lambda)_{\Sigma}$, 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 $\beta$-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 $\Sigma$-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 $\Sigma$-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.