Semantics-based Design and Correctness of
Control-flow Analysis-based Program Transformations


We show how control-flow-based program transformations in
functional languages can be proven correct.  The method relies
upon ``defunctionalization,'' a mapping from a higher-order
language to a first-order language.  We give methods for proving
defunctionalization correct.  Using this proof and common semantic
techniques, we then show how two program transformations---flow-based
inlining and lightweight defunctionalization---can be proven correct.

Joint work with Nevin Heintze and Jon G. Riecke.