Slicing polarized additive normalization

To attack the problem of “computing with the additives”, we introduce a notion of sliced proof-net for the polarized fragment of linear logic. We prove that this notion yields computational objects, sequentializable in the absence of cuts. We then show how the injectivity property of denotational semantics guarantees the “canonicity” of sliced proof-nets, and prove injectivity for the fragment of polarized linear logic corresponding to the simply typed λ-calculus with pairing.