Abstract |
This paper is a structured introduction to Intuitionistic Light Affine Logic (ILAL). ILAL has a polynomially costing normalization, and it is expressive enough to encode, and simulate, all PolyTime Turing machines. The bound on the normalization cost is proved by introducing the proof-nets for ILAL. The bound follows from a suitable normalization strategy that exploits structural properties of the proof-nets. This allows to have a good catch on the meaning of the paragraph modality, which is a peculiarity of light logics. The expressive power of ILAL is demonstrated in full details. Such a proof gives a flavor of the non trivial task of programming with resource limitations, using ILAL derivations as programs. |
@article{Asperti+Roversi:2002-ToCL,
number = {1},
volume = {3},
month = {January},
author = {Asperti, Andrea and Roversi, Luca},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2002-ToCL/AspertiRoversi2002ToCL.ps.gz},
abstract = {This paper is a structured introduction to Intuitionistic Light
Affine Logic (ILAL). ILAL has a polynomially costing
normalization, and it is expressive enough to encode, and
simulate, all PolyTime Turing machines. The bound on the
normalization cost is proved by introducing the proof-nets for
ILAL. The bound follows from a suitable normalization strategy
that exploits structural properties of the proof-nets. This allows
to have a good catch on the meaning of the paragraph modality,
which is a peculiarity of light logics. The expressive power of
ILAL is demonstrated in full details. Such a proof gives a flavor
of the non trivial task of programming with resource limitations,
using ILAL derivations as programs.},
title = {Intuitionistic Light Affine Logic},
year = {2002},
pages = {1 -- 39},
journal = {ACM Transactions on Computational Logic},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)