
Formal Methods in Computing (Most of the papers antecedent to 1995 are 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)  103116 
Year  2005 
ISSN number  15710661 
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 callbyname and callbyvalue $\lambda $calculus. In fact, it turns out that the class of lazy strongly $\beta $normalizing terms coincides with that of callbyvalue potentially valuable terms. This last class is of particular interest since it is a key notion for characterizing solvability in the callbyvalue setting. 
Download the complete article:
BibTeX code 
@inproceedings{paolini04itrs,
volume = {136C},
issn = {15710661},
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 callbyname and callbyvalue
$\lambda$calculus.\\ In fact, it turns out that the class of lazy
strongly $\beta$normalizing terms coincides with that of
callbyvalue potentially valuable terms. This last class is of
particular interest since it is a key notion for characterizing
solvability in the callbyvalue setting.},
localfile = {http://www.di.unito.it/~paolini/papers/lsn05.pdf},
title = {Lazy strong normalization},
year = 2005,
pages = {103116},
}

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