A system of interaction and structure IV: The exponentials and decomposition

Lutz Straburger, Alessio Guglielmi

Research output: Contribution to journalArticle

17 Citations (Scopus)

Abstract

We study a system, called NEL, which is themixed commutative/noncommutative linear logic BV augmented with linear logic's exponentials. Equivalently, NEL is MELL augmented with the noncommutative self-dual connective seq. In this article,we show a basic compositionality property ofNEL,which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next article of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs.
Original languageEnglish
Article number23
JournalACM Transactions on Computational Logic
Volume12
Issue number4
DOIs
Publication statusPublished - Jul 2011

Fingerprint Dive into the research topics of 'A system of interaction and structure IV: The exponentials and decomposition'. Together they form a unique fingerprint.

  • Cite this