Download the complete article:

@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},
}

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)