Open AccessA Simple Take on Typed Abstract Syntax in Haskell-like Languages
Author(s) -
Olivier Danvy,
Morten Rhiger
Publication year - 2000
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v7i34.20169
Subject(s) - haskell , programming language , normalization (sociology) , lambda calculus , computer science , abstract syntax , functional programming , abstract syntax tree , syntax , system f , typed lambda calculus , parsing , natural language processing , semantics (computer science) , sociology , anthropology
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.