@inproceedings{DalLago+Roversi+Vercelli:2009-LFCS,
  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/2009-LFCS/DaLagoRoversiVercelli-09LFCS.pdf},
  abstract = {Pure, or type-free, Linear Logic proof nets are Turing complete
              once cut-elimination is considered as computation. We introduce
              modal impredicativity as a new form of impredicativity causing the
              complexity of cut-elimination 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)