A Denotational Investigation of Defunctionalization

Lasse R. Nielsen

December 2000


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.


Last modified: 2003-06-08 by webmaster.