We show how a simple semantic characterization of normalization by evaluation for the λ β μ-calculus can be extended to a similar construction for normalization of terms in the computational λ-calculus. Specifically, we show that a suitable residualizing interpretation of base types, constants, and computational effects allows us to extract a syntactic normal form from a term's denotation. The required interpretation can itself be constructed as the meaning of a suitable functional program in an ML-like language, leading directly to a practical normalization algorithm. The results extend easily to product and sum types, and can be seen as a formal basis for call-by-value type-directed partial evaluation. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Filinski, A. (2001). Normalization by evaluation for the computational lambda-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2044 LNCS, pp. 151–165). Springer Verlag. https://doi.org/10.1007/3-540-45413-6_15
Mendeley helps you to discover research relevant for your work.