Normalization by Evaluation with Typed Abstract Syntax

Forfattere

  • Olivier Danvy
  • Morten Rhiger
  • Kristoffer H. Rose

DOI:

https://doi.org/10.7146/brics.v8i16.20473

Resumé

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.

Downloads

Publiceret

2001-05-16

Citation/Eksport

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