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

Lutz Straburger, Alessio Guglielmi

Research output: Contribution to journalArticle

  • 9 Citations

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.
LanguageEnglish
Article number23
JournalACM Transactions on Computational Logic
Volume12
Issue number4
DOIs
StatusPublished - Jul 2011

Fingerprint

Flow graphs
Linear Logic
Decomposition
Compositionality
Decompose
Cut-elimination
Flow Graphs
Interaction
Theorem
Proof by induction
Series

Cite this

A system of interaction and structure IV: The exponentials and decomposition. / Straburger, Lutz; Guglielmi, Alessio.

In: ACM Transactions on Computational Logic, Vol. 12, No. 4, 23, 07.2011.

Research output: Contribution to journalArticle

@article{28f9d748d53e4ceeb34d4a1d0f8a4dfd,
title = "A system of interaction and structure IV: The exponentials and decomposition",
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.",
author = "Lutz Straburger and Alessio Guglielmi",
year = "2011",
month = "7",
doi = "10.1145/1970398.1970399",
language = "English",
volume = "12",
journal = "ACM Transactions on Computational Logic",
issn = "1529-3785",
publisher = "Association for Computing Machinery",
number = "4",

}

TY - JOUR

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

AU - Straburger,Lutz

AU - Guglielmi,Alessio

PY - 2011/7

Y1 - 2011/7

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

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

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

UR - http://arxiv.org/pdf/0903.5259

UR - http://dx.doi.org/10.1145/1970398.1970399

U2 - 10.1145/1970398.1970399

DO - 10.1145/1970398.1970399

M3 - Article

VL - 12

JO - ACM Transactions on Computational Logic

T2 - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

SN - 1529-3785

IS - 4

M1 - 23

ER -