Helmut Seidl and Morten Heine Sørensen. Constraints to Stop Deforestation. Sci. Comput. Program., 32(1-3):73-107, 1998.
Wadler's deforestation algorithm eliminates intermediate data structures from functional programs. To be suitable for inclusion in a compiler, deforestation must terminate on all programs. Several techniques exist to ensure termination of deforestation on all first-order programs, but general techniques for higher-order programs were introduced only recently first by Hamilton and then by Marlow. We present a new technique for ensuring termination of deforestation on all higher-order programs that allows useful transformation steps prohibited in Hamilton's and Marlow's techniques. The technique uses a constraint-based higher-order control-flow analysis We also relate our technique to previous approaches to termination of first- and higher-order deforestation in some detail.