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

 paolini04itrs (In proceedings) Author(s) Luca Paolini, Elaine Pimentel and Simona Ronchi Della Rocca Title « Lazy strong normalization » In Proceedings of Intersection Types and Related Systems (ITRS'04), a Satellite Workshop of the Symposium on Logic in Computer Science (LICS'04) Series Electronic Notes in Theoretical Computer Science Volume 136C Page(s) 103-116 Year 2005 ISSN number 1571-0661 URL http://www.di.unito.it/~ronchi/papers/lsn.pdf
 Abstract Among all the reduction strategies for the untyped $\lambda$-calculus, the so called lazy $\beta$-evaluation is of particular interest due to its large applicability to functional programming languages (e.g. Haskell [?]). This strategy reduces only redexes not inside a lambda abstraction. The lazy strongly $\beta$- normalizing terms are the $\lambda$-terms that don't have infinite lazy $\beta$-reduction sequences. This paper presents a logical characterization of lazy strongly $\beta$-normalizing terms using intersection types. This characterization, besides being interesting by itself, allows an interesting connection between call-by-name and call-by-value $\lambda$-calculus. In fact, it turns out that the class of lazy strongly $\beta$-normalizing terms coincides with that of call-by-value potentially valuable terms. This last class is of particular interest since it is a key notion for characterizing solvability in the call-by-value setting.

 BibTeX code

@inproceedings{paolini04itrs,
volume = {136C},
issn = {1571-0661},
author = {Paolini, Luca and Pimentel, Elaine and Ronchi Della Rocca, Simona},
series = {Electronic Notes in Theoretical Computer Science},
booktitle = {Proceedings of Intersection Types and Related Systems (ITRS'04),
a Satellite Workshop of the Symposium on Logic in Computer
Science (LICS'04)},
url = {http://www.di.unito.it/~ronchi/papers/lsn.pdf},
tag = {Intersection Types and Related Systems 2004},
abstract = {Among all the reduction strategies for the untyped
$\lambda$-calculus, the so called {\em lazy $\beta$-evaluation} is
of particular interest due to its large applicability to
functional programming languages (e.g. Haskell~\cite{Bi98}). This
strategy reduces only redexes not inside a lambda abstraction.\\
The lazy strongly $\beta$- normalizing terms are the
$\lambda$-terms that don't have infinite lazy $\beta$-reduction
sequences.\\ This paper presents a logical characterization of
lazy strongly $\beta$-normalizing terms using intersection types.
This characterization, besides being interesting by itself, allows
an interesting connection between call-by-name and call-by-value
$\lambda$-calculus.\\ In fact, it turns out that the class of lazy
strongly $\beta$-normalizing terms coincides with that of
call-by-value potentially valuable terms. This last class is of
particular interest since it is a key notion for characterizing
solvability in the call-by-value setting.},
localfile = {http://www.di.unito.it/~paolini/papers/lsn05.pdf},
title = {Lazy strong normalization},
year = 2005,
pages = {103-116},
}

 Formal Methods in Computing(Most of the papers antecedent to 1995are 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)