Normalization by Evaluation with Typed Abstract Syntax

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