Defunctionalization at Work

Olivier Danvy, Lasse R. Nielsen


We study practical applications of Reynolds's defunctionalization technique, which is a whole-program transformation from higher-order to first-order functional programs. This study leads us to discover new connections between seemingly unrelated higher-order and first-order specifications and their correctness proofs. We thus perceive defunctionalization both as a springboard and as a bridge: as a springboard for discovering new connections between the first-order world and the higher-order world; and as a bridge for transferring existing results between first-order and higher-order settings.

Full Text:


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