Proof nets for bi-intuitionistic linear logic

Gianluigi Bellin, Willem Heijltjes

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)
13 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 languageEnglish
Title of host publication3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018
Subtitle of host publicationLeibnitz International proceedings in Informatics
EditorsHelene Kirchner
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages1-17
Number of pages17
Volume108
ISBN (Electronic)9783959770774
DOIs
Publication statusPublished - 1 Jul 2018

Publication series

NameLeibniz International Proceedings in Informations (LIPIcs)
PublisherSchloss Dagstuhl
ISSN (Print)1868-8969

Fingerprint

Proof Nets
Linear Logic
Intuitionistic Logic
Correctness
Tensor
Contractibility
Distributivity
Closed
Sequent Calculus
Subtraction
Rewriting
Multiplicative
Fragment
Logic
Unit
Demonstrate

Keywords

  • Contractibility
  • Intuitionistic linear logic
  • Linear logic
  • Proof nets

ASJC Scopus subject areas

  • Software

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). [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 in Book/Report/Conference proceedingConference contribution

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)). https://doi.org/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 = "7",
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 - Conference contribution

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 -