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.
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.
Original language | English |
---|---|
Title of host publication | 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018 |
Subtitle of host publication | Leibnitz International proceedings in Informatics |
Editors | Helene Kirchner |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Pages | 1-17 |
Number of pages | 17 |
Volume | 108 |
ISBN (Electronic) | 9783959770774 |
DOIs | |
Publication status | Published - 1 Jul 2018 |
Publication series
Name | Leibniz International Proceedings in Informations (LIPIcs) |
---|---|
Publisher | Schloss Dagstuhl |
ISSN (Print) | 1868-8969 |
Keywords
- Contractibility
- Intuitionistic linear logic
- Linear logic
- Proof nets
ASJC Scopus subject areas
- Software