Normalization by Evaluation with Typed Abstract Syntax | Zendy

Olivier Danvy | Zendy; Morten Rhiger | Zendy; Kristoffer H. Rose | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Normalization 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research