Relating categorical semantics for intuitionistic linear logic

Research output: Contribution to journalArticle

Authors

Colleges, School and Institutes

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.

Details

Original languageEnglish
Pages (from-to)1-36
Number of pages36
JournalApplied Categorical Structures
Volume13
Issue number1
Publication statusPublished - 1 Jan 2005