TY - JOUR AU - Danvy, Olivier AU - Rhiger, Morten PY - 2000/06/04 Y2 - 2024/03/29 TI - A Simple Take on Typed Abstract Syntax in Haskell-like Languages JF - BRICS Report Series JA - BRICS VL - 7 IS - 34 SE - Articles DO - 10.7146/brics.v7i34.20169 UR - https://tidsskrift.dk/brics/article/view/20169 SP - AB - <p>We present a simple way to program typed abstract syntax in a <br />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.</p><p>Keywords: Type-directed partial evaluation, normalization functions, simply-typed lambda-calculus, higher-order abstract syntax, Haskell.</p> ER -