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,