Olivier Laurent and Lorenzo Tortora de Falco. Slicing polarized additive normalization. Quaderno 12, Istituto per le Applicazioni del Calcolo, Roma, Italy, June 2001. To appear in Linear Logic in Computer Science, Thomas Ehrhard, Jean-Yves Girard, Paul Ruet and Phil Scott editors, London Mathematical Society Lecture Notes Series, Cambridge University Press.

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 simply typed lambda-calculus with pairing.

[ bib | .html ]

Back