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: |