Happy new year!

Hello Frogs,

What you all have been waiting for for five years is finally a reality:

http://www.lix.polytechnique.fr/~lutz/papers/NELbig.pdf

It is the first paper that contains a readable proof of the decomposition 
theorems and it is the first paper that contains a splitting proof 
involving exponentials.

Any comments about this new version of an old paper are, of course, 
very welcome.

Best wishes for the new year,
Lutz

*******************************************************

Title: "A System of Interaction and Structure IV: The Exponentials"

Authors: Alessio Guglielmi and Lutz Straßburger

Abstract: We study some normalisation properties of the deep-inference 
proof system NEL, which can be seen both as 1) an extension of 
multiplicative exponential linear logic (MELL) by a certain 
non-commutative self-dual logical operator; and 2) an extension of system 
BV by the exponentials of linear logic. The interest of NEL resides in: 1) 
its being Turing complete, while the same for MELL is not known, and is 
widely conjectured not to be the case; 2) its inclusion of a self-dual, 
non-commutative logical operator that, despite its simplicity, cannot be 
axiomatised in any analytic sequent calculus system; 3) its ability to 
model the sequential composition of processes. We present several 
decomposition results for NEL and, as a consequence of those and via a 
splitting theorem, cut elimination. We use, for the first time, an 
induction measure based on flow graphs associated to the exponentials, 
which captures their rather complex behaviour in the normalisation 
process. The results are presented in the calculus of structures, which is 
the first, developed formalism in deep inference.


(This paper was previously titled "A Non-commutative Extension of 
Multiplicative Exponential Linear Logic" and is the journal version of "A 
Non-commutative Extension of MELL")