TY - JOUR
T1 - Relating categorical semantics for intuitionistic linear logic
AU - Maietti, M
AU - Mannegia, P
AU - de Paiva, V
AU - Ritter, Eike
PY - 2005/1/1
Y1 - 2005/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=14844366173&partnerID=8YFLogxK
U2 - 10.1007/s10485-004-3134-z
DO - 10.1007/s10485-004-3134-z
M3 - Article
VL - 13
SP - 1
EP - 36
JO - Applied Categorical Structures
JF - Applied Categorical Structures
IS - 1
ER -