TY - JOUR AU - Nielsen, Lasse R. PY - 2000/06/17 Y2 - 2024/03/28 TI - A Denotational Investigation of Defunctionalization JF - BRICS Report Series JA - BRICS VL - 7 IS - 47 SE - Articles DO - 10.7146/brics.v7i47.20214 UR - https://tidsskrift.dk/brics/article/view/20214 SP - AB - <p>Defunctionalization was introduced by John Reynolds in his 1972<br />article Definitional Interpreters for Higher-Order Programming <br />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.</p><p>Keywords: defunctionalization, program transformation, denotational semantics, logical relations.</p> ER -