非表示:
キーワード:
-
要旨:
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.
