A system of interaction and structure V: the exponentials and splitting

Alessio Guglielmi, L Straburger

Research output: Contribution to journalArticlepeer-review

16 Citations (SciVal)
177 Downloads (Pure)


System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. NEL is presented in deep inference, because no Gentzen formalism can express it in such a way that the cut rule is admissible. Other recent work shows that system NEL is Turing-complete, and is able to express process algebra sequential composition directly and model causal quantum evolution faithfully. In this paper, we show cut elimination for NEL, based on a technique that we call splitting. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. When combined with a 'decomposition' theorem, proved in the previous paper of this series, splitting yields a cut-elimination procedure for NEL.
Original languageEnglish
Pages (from-to)563-584
Number of pages22
JournalMathematical Structures in Computer Science
Issue number3
Publication statusPublished - Jun 2011


Dive into the research topics of 'A system of interaction and structure V: the exponentials and splitting'. Together they form a unique fingerprint.

Cite this