A Simple Take on Typed Abstract Syntax in Haskell-like Languages

Olivier Danvy
Morten Rhiger

December 2000


We present a simple way to program typed abstract syntax in a language following a Hindley-Milner typing discipline, such as ML and Haskell, and we apply it to automate two proofs about normalization functions as embodied in type-directed partial evaluation for the simply typed lambda calculus: (1) normalization functions preserve types and (2) they yield long beta-eta normal forms

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.