| 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. |
@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},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
