Relating Categorical Semantics for Intuitionistic Linear Logic

There are several kinds of linear typed calculus in the literature, some with their associated notion of categorical model. Our aim in this paper is to systematise the relationship between three of these linear typed calculi and their models. We point out that mere soundness and completeness of a linear typed calculus with respect to a class of categorical models are not sufficient to identify the most appropriate class uniquely. We recommend instead to use the notion of internal language when relating a typed calculus to a class of models. After clarifying the internal languages of the categories of models in the literature we relate these models via reflections and coreflections. Key words: intuitionistic linear logic, typed lambda calculus, symmetric monoidal closed categories, symmetric monoidal adjunctions. AMS classifications: 03G30 03B15 18C50 03B20

• Type: Journal
• Year: 2005
• Where: ACS
• Authors: Maria Emilia Maietti, Paola Maneggia, Valeria de Paiva, Eike Ritter
• Keywords: ACS 2005, ACS 2007, Categorical Models, Internal Languages, Linear Typed Calculus