On the categorical semantics of elementary linear logic

Olivier Laurent

We introduce the notion of elementary Seely category as a notion of categorical model of Elementary Linear Logic (ELL) inspired from Seely's definition of models of Linear Logic (LL). In order to deal with additive connectives in ELL, we use the approach of Danos and Joinet. From the categorical point of view, this requires us to go outside the usual interpretation of connectives by functors. The $!$ connective is decomposed into a pre-connective $\sharp$ which is interpreted by a whole family of functors (generated by $\id$, $\tens$ and $\with$). As an application, we prove the stratified coherent model and the obsessional coherent model to be elementary Seely categories and thus models of ELL.

Keywords: monoidal categories, elementary linear logic, categorical logic, denotational semantics, coherent spaces

2000 MSC: 18C50

Theory and Applications of Categories, Vol. 22, 2009, No. 10, pp 269-301.


TAC Home