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.
Relating Categorical Semantics for Intuitionistic Linear Logic
MAIETTI, MARIA EMILIA;
2005
Abstract
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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.