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
SN - 1529-3785
VL - 12
JO - ACM Transactions on Computational Logic
JF - ACM Transactions on Computational Logic
IS - 4
M1 - 23
ER -