Cut Elimination for Monomial MALL Proof Nets

We present a syntax for MALL (multiplicative additive linear logic without units) proof nets which refines Girard´s one. It is also based on the use of monomial weights for identifying additive components (slices). Our generalization gives the possibility of representing a kind of sharing of nodes which does not exist in Girard´s nets. This sharing leads to the definition of a strong cut elimination procedure for MALL. We give a correctness criterion which is proved to be stable by reduction and to give a sequentialization theorem with respect to the sequent calculus. Sequentialization is proved by showing that an expansion procedure allows us to unfold any of our proof nets into a Girard proof net.