FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Around Classical and Intuitionistic Linear Logics

Author: Olivier Laurent

Paper Information

Title:Around Classical and Intuitionistic Linear Logics
Authors:Olivier Laurent
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Linear logic, Intuitionistic linear logic, Tensor logic, Negative translations, Double negation, Focusing, Conservativity
Abstract:

ABSTRACT. We revisit many aspects of the syntactic relations between (variants of) classical linear logic (LL) and (variants of) intuitionistic linear logic (ILL) in the propositional setting.

On the one hand, we study different (parametric) ``negative'' translations from LL to ILL: their expressiveness, the relations with extensions of LL and their use in the proof theory of LL (cut elimination and focusing). In particular, this bridges the intuitionistic restriction on sequents (at most one conclusion) and the focusing property of linear logic. On the other hand, we generalise the known partial results about conservativity of LL over ILL, leading for example to a conservativity proof for LL over tensor logic (TL).

Pages:10
Talk:Jul 10 15:00 (Session 55E)
Paper: