| Abstract |
| We study the relations between Multiplicative Exponential Linear Logic (MELL) and Baillot-Mazza Linear Logic by Levels (). We design a decoration-based translation between propositional MELL and propositional . The translation preserves the cut elimination. Moreover, we show that there is a proof net of second order MELL that cannot have a representative in second order under any decoration. This suggests that levels can be an analytical tool in understanding the complexity of second order quantifier. |
@inproceedings{Gaboardi-Roversi+Vercelli:2009-MFCS09,
volume = {5734},
author = {Gaboardi, Marco and Roversi, Luca and Vercelli, Luca},
note = {To appear},
series = {Lecture Notes in Computer Science},
booktitle = {{P}roceedings of {MFCS'09}},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2009-MFCS/GaboardiRoversiVercelli2009MFCS.pdf},
abstract = {We study the relations between Multiplicative Exponential Linear
Logic (\textsf{MELL}) and Baillot-Mazza Linear Logic by Levels
($\mathsf{ML}^3$). We design a decoration-based translation
between propositional \textsf{MELL} and propositional
$\mathsf{ML}^3$. The translation preserves the cut elimination.
Moreover, we show that there is a proof net $\Pi$ of second order
\textsf{MELL} that cannot have a representative $\Pi'$ in second
order $\mathsf{ML}^3$ under any decoration. This suggests that
levels can be an analytical tool in understanding the complexity
of second order quantifier. },
title = {{A by-level analysis of Multiplicative Exponential Linear Logic}},
publisher = {Springer},
pages = {344 -- 355},
year = {2009},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
