|
Defunctionalization at Work
Olivier Danvy
June 2001 |
Abstract:
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
Available as PostScript, PDF, DVI. |