Abstract
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.
Author supplied keywords
Cite
CITATION STYLE
Danvy, O., & Rhiger, M. (2001). A simple take on typed abstract syntax in Haskell-like languages. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2024, pp. 343–358). Springer Verlag. https://doi.org/10.1007/3-540-44716-4_22
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
