@article{BasinAnderson00,
TITLE = "Program Development Schemata as Derived Rules",
AUTHOR = {Anderson, Penny and Basin, David},
JOURNAL ="Journal of Symbolic Computation",
MONTH = "July",
YEAR = "2000",
VOLUME = 30,
Number = 1,
Pages="5--36",
ABSTRACT = {
  We show how the formalization and application of schemata for program
  development can be reduced to the formalization and application of
  derived rules of inference.  We formalize and derive schemata as rules
  in theories that axiomatize program data and programs themselves.  We
  reduce schema-based program development to ordinary theorem proving,
  where higher-order unification is used to apply rules.  Conceptually,
  our formalization is simple and unifies divergent views of schemata,
  program synthesis, and program transformation.
  Practically, our formalization yields a simple methodology for
  carrying out development using existing logical frameworks; we
  illustrate this in the domain of logic program synthesis and
  transformation using the Isabelle logical framework.}
}