Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

Roversi+Vercelli:2009-TYPES08 (In proceedings)
Author(s) Luca Roversi and Luca Vercelli
Title« Some Complexity and Expressiveness results on Multimodal and Stratified Proof-nets »
InProceedings of TYPES'08
SeriesLecture Notes in Computer Science
Volume5497
Page(s)306 -- 322
Year2009
PublisherSpringer
URLhttp://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2009-TYPES08/RoversiVercelli-TYPES08.pdf
NoteTo appear
Abstract
We introduce a multimodal stratified framework MS that generalizes an idea hidden in the definitions of Light Linear/Affine logics: ``More modalities means more expressiveness''. MS is a set of building rule schemes that depend on parameters. We interpret the values of the parameters as modalities. Fixing the parameters yields deductive systems as instances of MS, that we call subsystems. Every subsystem generates stratified proof-nets whose normalization preserves stratification, a structural property of nodes and edges, like in Light Linear/Affine logics. A first result is a sufficient condition for determining when a subsystem is strongly polynomial time sound. A second one shows that the ability to choose which modalities are used and how can be rewarding. We give a family of subsystems as complex as Multiplicative Linear Logic â they are linear time and space sound â that can represent Church numerals and some common combinators on them.

BibTeX code

@inproceedings{Roversi+Vercelli:2009-TYPES08,
  volume = {5497},
  author = {Roversi, Luca and Vercelli, Luca},
  note = {To appear},
  series = {Lecture Notes in Computer Science},
  booktitle = {{P}roceedings of {TYPES'08}},
  url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2009-TYPES08/RoversiVercelli-TYPES08.pdf},
  abstract = {We introduce a multimodal stratified framework MS that generalizes
              an idea hidden in the definitions of Light Linear/Affine logics:
              ``More modalities means more expressiveness''. MS is a set of
              building rule schemes that depend on parameters. We interpret the
              values of the parameters as modalities. Fixing the parameters
              yields deductive systems as instances of MS, that we call
              subsystems. Every subsystem generates stratified proof-nets whose
              normalization preserves stratification, a structural property of
              nodes and edges, like in Light Linear/Affine logics. A first
              result is a sufficient condition for determining when a subsystem
              is strongly polynomial time sound. A second one shows that the
              ability to choose which modalities are used and how can be
              rewarding. We give a family of subsystems as complex as
              Multiplicative Linear Logic — they are linear time and space
              sound — that can represent Church numerals and some common
              combinators on them. },
  title = {{Some Complexity and Expressiveness results on Multimodal and
           Stratified Proof-nets}},
  publisher = {Springer},
  pages = {306 -- 322},
  year = {2009},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!