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.