Normalization by Evaluation with Typed Abstract Syntax

Authors

  • Olivier Danvy
  • Morten Rhiger
  • Kristoffer H. Rose

DOI:

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

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.

Downloads

Published

2001-05-16

How to Cite

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

Issue

No. 16 (2001): RS-16 Normalization by Evaluation with Typed Abstract Syntax

Section

Articles

License

Creative Commons License

Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.