|
A Simple Take on Typed Abstract Syntax in Haskell-like Languages
Olivier Danvy
December 2000 |
Abstract:
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. |