The Hot List Strategy*
An Algorithm for General Set Unification and Its Complexity
Recursive Program Optimization through Inductive Synthesis Proof Transformation*