Relating categorical semantics for intuitionistic linear logic

M Maietti, P Mannegia, V de Paiva, Eike Ritter

Research output: Contribution to journalArticle

16 Citations (Scopus)


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.
Original languageEnglish
Pages (from-to)1-36
Number of pages36
JournalApplied Categorical Structures
Issue number1
Publication statusPublished - 1 Jan 2005


Dive into the research topics of 'Relating categorical semantics for intuitionistic linear logic'. Together they form a unique fingerprint.

Cite this