Slicing polarized additive normalization
Laurent, Olivier ; Tortora De Falco, Lorenzo
HAL, hal-00009134 / Harvested from HAL
Text on HAL
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 lambda-calculus with pairing.
Publié le : 2004-07-05
Classification:  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO],  [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 
@article{hal-00009134,
     author = {Laurent, Olivier and Tortora De Falco, Lorenzo},
     title = {Slicing polarized additive normalization},
     journal = {HAL},
     volume = {2004},
     number = {0},
     year = {2004},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-00009134}
}

Laurent, Olivier; Tortora De Falco, Lorenzo. Slicing polarized additive normalization. HAL, Tome 2004 (2004) no. 0, . http://gdmltest.u-ga.fr/item/hal-00009134/