A Categorical Semantics for Linear Logical Frameworks

TL;DR

This paper introduces a new type theory combining linear types with dependent types, providing a categorical semantics framework that unifies intuitionistic dependent type theory and linear logic.

Contribution

It develops a syntax and complete categorical semantics for the combined type theory, including modular treatment of various type formers and natural emergence of multiplicative quantifiers.

Findings

Categorical semantics in terms of indexed symmetric monoidal categories with comprehension.

Natural emergence of multiplicative quantifiers and identity types from categorical considerations.

Analysis of models with values in symmetric monoidal categories.

Abstract

A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In particular, we see that the historically much-debated multiplicative quantifiers and identity types arise naturally from categorical considerations. These new multiplicative connectives are further characterised by several identities relating them to the usual connectives from dependent type theory and linear logic. Finally, one important class of models, given by families with values in some symmetric monoidal category, is investigated in detail.