文章基本信息

标题：A Simple Take on Typed Abstract Syntax in Haskell-like Languages
本地全文：下载
作者：Olivier Danvy ; Morten Rhiger
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：2000
卷号：7
期号：34
出版社：Aarhus University
摘要：We present a simple way to program typed abstract syntax in a language following a Hindley-Milner typing discipline, such as Haskell and ML, and we apply it to automate two proofs about normalization functions as embodied in type-directed partial evaluation for the simply typed lambda calculus: normalization functions (1) preserve types and (2) yield long beta-eta normal forms. Keywords: Type-directed partial evaluation, normalization functions, simply-typed lambda-calculus, higher-order abstract syntax, Haskell.