Open AccessNormalization by Evaluation with Typed Abstract Syntax
Author(s) -
Olivier Danvy,
Morten Rhiger,
Kristoffer H. Rose
Publication year - 2001
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v8i16.20473
Subject(s) - normalization (sociology) , haskell , programming language , syntax , computer science , abstract syntax , abstract syntax tree , system f , functional programming , typed lambda calculus , lambda calculus , mathematics , algorithm , natural language processing , parsing , semantics (computer science) , sociology , anthropology
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.