A Denotational Investigation of Defunctionalization - Nielsen, Lasse R. (BRICS Report Series, 2000)
Defunctionalization was introduced by John Reynolds in his 1972 article Definitional Interpreters for Higher-Order Programming Languages. Defunctionalization transforms a higher-order program into a first-order one, representing functional values as data structures. Since then it has been used quite widely, but 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. Keywords: defunctionalization, program transformation, denotational semantics, logical relations.