Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2018.10
URN: urn:nbn:de:0030-drops-91800
URL: https://drops.dagstuhl.de/opus/volltexte/2018/9180/
Bellin, Gianluigi ; Heijltjes, Willem B.
Proof Nets for Bi-Intuitionistic Linear Logic
| pdf-format: |
|
Abstract
Bi-Intuitionistic Linear Logic (BILL) is an extension of Intuitionistic Linear Logic with a par, dual to the tensor, and subtraction, dual to linear implication. It is the logic of categories with a monoidal closed and a monoidal co-closed structure that are related by linear distributivity, a strength of the tensor over the par. It conservatively extends Full Intuitionistic Linear Logic (FILL), which includes only the par. We give proof nets for the multiplicative, unit-free fragment MBILL-. Correctness is by local rewriting in the style of Danos contractibility, which yields sequentialization into a relational sequent calculus extending the existing one for FILL. We give a second, geometric correctness condition combining Danos-Regnier switching and Lamarche's Essential Net criterion, and demonstrate composition both inductively and as a one-off global operation.
BibTeX - Entry
@InProceedings{bellin_et_al:LIPIcs:2018:9180,
author = {Gianluigi Bellin and Willem B. Heijltjes},
title = {{Proof Nets for Bi-Intuitionistic Linear Logic}},
booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-077-4},
ISSN = {1868-8969},
year = {2018},
volume = {108},
editor = {H{\'e}l{\`e}ne Kirchner},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9180},
URN = {urn:nbn:de:0030-drops-91800},
doi = {10.4230/LIPIcs.FSCD.2018.10},
annote = {Keywords: proof nets, intuitionistic linear logic, contractibility, linear logic}
}
| Keywords: | proof nets, intuitionistic linear logic, contractibility, linear logic | |
| Seminar: | 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) | |
| Issue date: | 2018 | |
| Date of publication: | 04.07.2018 |
