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
Extended version available as the technical report BRICS RS-00-34.
Basic Research in Computer Science (http://www.brics.dk/), Centre of the Danish National Research Foundation.
Acknowledgments This work is supported by the ESPRIT Working Group APPSEM (http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/). Part
of it was carried out while the second author was visiting Jason Hickey at Caltech, in the summer and fall of 2000. We are
grateful to the anonymous reviewers and to Julia Lawall for perceptive comments.