Multiple conclusion linear logic: Cut elimination and more

Harley Eades, Valeria de Paiva

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

4 Scopus citations


Full Intuitionistic Linear Logic (FILL) was first introduced by Hyland and de Paiva, and went against current beliefs that it was not possible to incorporate all of the linear connectives, e.g. tensor, par, and implication, into an intuitionistic linear logic. It was shown that their formalization of FILL did not enjoy cut-elimination by Bierman, but Bellin proposed a change to the definition of FILL in the hope to regain cut-elimination. In this note we adopt Bellin’s proposed change and give a direct proof of cut-elimination. Then we show that a categorical model of FILL in the basic dialectica category is also a LNL model of Benton and a full tensor model of Melli`es’ and Tabareau’s tensorial logic. Lastly, we give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor.

Original languageEnglish (US)
Title of host publicationLogical Foundations of Computer Science - International Symposium, LFCS 2016, Proceedings
EditorsAnil Nerode, Sergei Artemov
PublisherSpringer Verlag
Number of pages16
ISBN (Print)9783319276823
StatePublished - 2016
EventInternational Symposium on Logical Foundations of Computer Science, LFCS 2016 - Deerfield Beach, United States
Duration: Jan 4 2016Jan 7 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


OtherInternational Symposium on Logical Foundations of Computer Science, LFCS 2016
Country/TerritoryUnited States
CityDeerfield Beach


  • Categorical model
  • Classical linear logic
  • Cut-elimination
  • Dialectica category
  • Full intuitionistic linear logic
  • Linear/non-linear models
  • Par
  • Proof theory
  • Tensorial logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Multiple conclusion linear logic: Cut elimination and more'. Together they form a unique fingerprint.

Cite this