Normalization by Evaluation with Typed Abstract Syntax

  • Olivier Danvy
  • Morten Rhiger
  • Kristoffer H. Rose

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.

Published
2001-05-16
How to Cite
Danvy, O., Rhiger, M., & Rose, K. (2001). Normalization by Evaluation with Typed Abstract Syntax. BRICS Report Series, 8(16). https://doi.org/10.7146/brics.v8i16.20473