Ronchi Della Rocca S. Paolini L., Pimentel E.
Lazy
strong normalization
In Proceedings of Intersection Types and Related System. A
satellite workshops of the Joint Meeting ICALP2004/LICS2004., volume to
appear, page ??, 2004
Mario Coppo and Damiani Ferruccio editors.
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.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43