DalLago+Roversi+Vercelli:2009LFCS (In proceedings)

Author(s)  Ugo Dal Lago, Luca Roversi and Luca Vercelli 
Title  « Taming Modal Impredicativity: Superlazy Reduction » 
In  Proceedings of Logical Foundations of Computer Science (LFCS09) 
Series  Lecture Notes in Computer Science 
Volume  LNCS 5407 
Page(s)  137  151 
Year  2009 
Publisher  Springer Verlag 
URL  http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2009LFCS/DaLagoRoversiVercelli09LFCS.pdf 
Note  An extended version is http://arxiv.org/abs/0810.2891 
Abstract 
Pure, or typefree, Linear Logic proof nets are Turing complete once cutelimination is considered as computation. We introduce modal impredicativity as a new form of impredicativity causing the complexity of cutelimination to be problematic from a complexity point of view. Modal impredicativity occurs when, during reduction, the conclusion of a residual of a box b interacts with a node that belongs to the proof net inside another residual of b. Technically speaking, superlazy reduction is a new notion of reduction that allows to control modal impredicativity. More specifically, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of reducing a proof net finite and predictable. Specifically, superlazy reduction applied to any pure proof nets takes primitive recursive time. Moreover, any primitive recursive function can be computed by a pure proof net via superlazy reduction. 
@inproceedings{DalLago+Roversi+Vercelli:2009LFCS,
volume = {LNCS 5407},
month = {January},
author = {Dal Lago, Ugo and Roversi, Luca and Vercelli, Luca},
note = {An extended version is http://arxiv.org/abs/0810.2891},
series = {Lecture Notes in Computer Science},
booktitle = {{P}roceedings of {L}ogical {F}oundations of {C}omputer {S}cience
(LFCS09)},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2009LFCS/DaLagoRoversiVercelli09LFCS.pdf},
abstract = {Pure, or typefree, Linear Logic proof nets are Turing complete
once cutelimination is considered as computation. We introduce
modal impredicativity as a new form of impredicativity causing the
complexity of cutelimination to be problematic from a complexity
point of view. Modal impredicativity occurs when, during
reduction, the conclusion of a residual of a box b interacts with
a node that belongs to the proof net inside another residual of b.
Technically speaking, superlazy reduction is a new notion of
reduction that allows to control modal impredicativity. More
specifically, superlazy reduction replicates a box only when all
its copies are opened. This makes the overall cost of reducing a
proof net finite and predictable. Specifically, superlazy
reduction applied to any pure proof nets takes primitive recursive
time. Moreover, any primitive recursive function can be computed
by a pure proof net via superlazy reduction. },
title = {{T}aming {M}odal {I}mpredicativity: {S}uperlazy {R}eduction},
copyrightspringer = {http://www.springer.de/comp/lncs/index.html},
publisher = {Springer Verlag},
pages = {137  151},
year = {2009},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)