文章基本信息

标题：Normalization by Evaluation with Typed Abstract Syntax
本地全文：下载
作者：Olivier Danvy ; Morten Rhiger ; Kristoffer H. Rose 等
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：2001
卷号：8
期号：16
出版社：Aarhus University
摘要：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.