| Abstract |
| The thesis focuses mainly on two subjects. The principal one is the introduction and the study of a functional language, called lambdaL, having two main features. Firstly, lambdaL is as much expressive as the call-by-value lambda-Calculus. Secondly, lambdaL enjoys the resource-awareness of the typed/typable functional languages, encoding the Intuitionistic Linear Logic. One-Step, Multi-Step and Denotational Semantics are defined for lambdaL, and a theoretical tool for deriving Multi-Step operational equivalences from denotational equivalences is developed. The core of the theoretical tool are an Approximation Theorem, and a Type Assignment for lambdaL. The Approximation Theorem is the bridge between an inductive syntactic representation of a canonical denotational model for the terms of lambdaL, and the computational behavior of lambdaL. It is proved using techniques borrowed from the Candidates of Reducibility. The Type Assignment is the inductive syntactic representation of a canonical denotational model. It deduces formulas which belong to a restriction of the intersection types to the terms of lambdaL. The second subject of the thesis is a natural deduction, called N, for Intuitionistic Linear Logic. N has half commuting conversions that the most popular natural deduction for Intuitionistic Linear Logic, given by Benton, Bierman, de Paiva, and Hyland. This is equivalent to saying that N improves the description of the Curry-Howard principle, applied to Intuitionistic Linear Logic. |
@inproceedings{Pravato-Roversi:1995-ICTCS,
booktitle = {Fifth Italian Conference on Theoretical Computer Science},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/1995-ICTCS/PravatoRoversi1995ICTCS.ps.gz},
abstract = {The thesis focuses mainly on two subjects. The principal one is
the introduction and the study of a functional language, called
lambdaL, having two main features. Firstly, lambdaL is as much
expressive as the call-by-value lambda-Calculus. Secondly, lambdaL
enjoys the resource-awareness of the typed/typable functional
languages, encoding the Intuitionistic Linear Logic. One-Step,
Multi-Step and Denotational Semantics are defined for lambdaL, and
a theoretical tool for deriving Multi-Step operational
equivalences from denotational equivalences is developed. The core
of the theoretical tool are an Approximation Theorem, and a Type
Assignment for lambdaL. The Approximation Theorem is the bridge
between an inductive syntactic representation of a canonical
denotational model for the terms of lambdaL, and the computational
behavior of lambdaL. It is proved using techniques borrowed from
the Candidates of Reducibility. The Type Assignment is the
inductive syntactic representation of a canonical denotational
model. It deduces formulas which belong to a restriction of the
intersection types to the terms of lambdaL. The second subject of
the thesis is a natural deduction, called N, for Intuitionistic
Linear Logic. N has half commuting conversions that the most
popular natural deduction for Intuitionistic Linear Logic, given
by Benton, Bierman, de Paiva, and Hyland. This is equivalent to
saying that N improves the description of the Curry-Howard
principle, applied to Intuitionistic Linear Logic.},
address = {Salerno (Italy)},
title = {$\Lambda_!$ considered both as a paradigmatic language and as a
meta-language},
author = {Pravato, Alberto and Roversi, Luca},
year = {1995},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
