Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis

Richard Waldinger

The unification algorithm has long been a target for program synthesis research, but a fully automatic derivation remains a research goal. In deductive program synthesis, computer…