|
A Denotational Investigation of Defunctionalization
Lasse R. Nielsen December 2000 |
Abstract:
Defunctionalization has been introduced by John Reynolds in his
1972 article Definitional Interpreters for Higher-Order Programming
Languages. Its goal is to transform a higher-order program into a
first-order one, representing functional values as data structures. Even
though defunctionalization has been widely used, we observe that it has never
been proven correct. We formalize defunctionalization denotationally for a
typed functional language, and we prove that it preserves the meaning of any
terminating program. Our proof uses logical relations
Available as PostScript, PDF, DVI. |