Proof nets for bi-intuitionistic linear logic

Gianluigi Bellin; Willem Heijltjes

doi:10.4230/LIPIcs.FSCD.2018.10

Proof nets for bi-intuitionistic linear logic

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

3 Citations (SciVal)

86 Downloads (Pure)

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.

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	https://doi.org/10.4230/LIPIcs.FSCD.2018.10
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

Access to Document

10.4230/LIPIcs.FSCD.2018.10Licence: CC BY

BILLAccepted author manuscript, 248 KBLicence: CC BY

Cite this

Bellin, G., & Heijltjes, W. (2018). Proof nets for bi-intuitionistic linear logic. In H. Kirchner (Ed.), 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018: Leibnitz International proceedings in Informatics (Vol. 108, pp. 1-17). Article 10 (Leibniz International Proceedings in Informations (LIPIcs)). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2018.10

Proof nets for bi-intuitionistic linear logic. / Bellin, Gianluigi; Heijltjes, Willem.
3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018: Leibnitz International proceedings in Informatics. ed. / Helene Kirchner. Vol. 108 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2018. p. 1-17 10 (Leibniz International Proceedings in Informations (LIPIcs)).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Bellin, G & Heijltjes, W 2018, Proof nets for bi-intuitionistic linear logic. in H Kirchner (ed.), 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018: Leibnitz International proceedings in Informatics. vol. 108, 10, Leibniz International Proceedings in Informations (LIPIcs), Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 1-17. https://doi.org/10.4230/LIPIcs.FSCD.2018.10

Bellin G, Heijltjes W. Proof nets for bi-intuitionistic linear logic. In Kirchner H, editor, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018: Leibnitz International proceedings in Informatics. Vol. 108. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2018. p. 1-17. 10. (Leibniz International Proceedings in Informations (LIPIcs)). doi: 10.4230/LIPIcs.FSCD.2018.10

Bellin, Gianluigi ; Heijltjes, Willem. / Proof nets for bi-intuitionistic linear logic. 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018: Leibnitz International proceedings in Informatics. editor / Helene Kirchner. Vol. 108 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2018. pp. 1-17 (Leibniz International Proceedings in Informations (LIPIcs)).

@inproceedings{51568d5b1b694d709efb058759f3e5af,

title = "Proof nets for bi-intuitionistic linear logic",

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.",

keywords = "Contractibility, Intuitionistic linear logic, Linear logic, Proof nets",

author = "Gianluigi Bellin and Willem Heijltjes",

year = "2018",

month = jul,

day = "1",

doi = "10.4230/LIPIcs.FSCD.2018.10",

language = "English",

volume = "108",

series = "Leibniz International Proceedings in Informations (LIPIcs)",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

pages = "1--17",

editor = "Helene Kirchner",

booktitle = "3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018",

address = "Germany",

}

TY - GEN

T1 - Proof nets for bi-intuitionistic linear logic

AU - Bellin, Gianluigi

AU - Heijltjes, Willem

PY - 2018/7/1

Y1 - 2018/7/1

N2 - 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.

AB - 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.

KW - Contractibility

KW - Intuitionistic linear logic

KW - Linear logic

KW - Proof nets

UR - http://www.scopus.com/inward/record.url?scp=85049792203&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.FSCD.2018.10

DO - 10.4230/LIPIcs.FSCD.2018.10

M3 - Chapter in a published conference proceeding

VL - 108

T3 - Leibniz International Proceedings in Informations (LIPIcs)

SP - 1

EP - 17

BT - 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018

A2 - Kirchner, Helene

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -

Proof nets for bi-intuitionistic linear logic

Abstract

Publication series

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this