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.