Normalization by Evaluation for the Compuational Lambda-Calculus
We show how a simple semantic characterization of normalization by
evaluation for the $\lambda_{\beta\eta}$-calculus
can be extended to a similar construction for normalization of terms
in the computational $\lambda$-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.
Full document:
DVI or
PostScript.