A Denotational Investigation of Defunctionalization

Forfattere

  • Lasse R. Nielsen

DOI:

https://doi.org/10.7146/brics.v7i47.20214

Resumé

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.

Downloads

Publiceret

2000-06-17

Citation/Eksport

Nielsen, L. R. (2000). A Denotational Investigation of Defunctionalization. BRICS Report Series, 7(47). https://doi.org/10.7146/brics.v7i47.20214