Proof nets for bi-intuitionistic linear logic

Gianluigi Bellin, Willem Heijltjes

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

3 Citations (SciVal)
60 Downloads (Pure)


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
Number of pages17
ISBN (Electronic)9783959770774
Publication statusPublished - 1 Jul 2018

Publication series

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


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

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Proof nets for bi-intuitionistic linear logic'. Together they form a unique fingerprint.

Cite this