Normalization by Evaluation with Typed Abstract Syntax
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
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.