文章基本信息

标题：A Denotational Investigation of Defunctionalization
本地全文：下载
作者：Lasse R. Nielsen
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：2000
卷号：7
期号：47
出版社：Aarhus University
摘要：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.