Normalization by Evaluation with Typed Abstract Syntax - Danvy, Olivier; Rhiger, Morten; Rose, Kristoffer H. (BRICS Report Series, 2001)
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.