Normalization by Evaluation with Typed Abstract Syntax

Olivier Danvy
Morten Rhiger
Kristoffer H. Rose

May 2001

Abstract:

We present a simple way to implement typed abstract syntax for the lambda calculus in Haskell, using phantom types, and we specify normalization by evaluation (i.e., type-directed partial evaluation) to yield this typed abstract syntax. Proving that normalization by evaluation preserves types and yields normal forms then reduces to type-checking the specification

Available as PostScript, PDF, DVI.

Last modified: 2003-06-08 by webmaster.