A Denotational Investigation of Defunctionalization

Lasse R. Nielsen


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.

Full Text:


DOI: http://dx.doi.org/10.7146/brics.v7i47.20214
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library