@INPROCEEDINGS{Anderson&Basin,
AUTHOR = "Penny Anderson and David Basin",
TITLE = "Deriving and Applying Logic Program Transformers",
BOOKTITLE = "Algorithms, Concurrency and Knowledge  (1995 Asian Computing Science Conference)",
ADDRESS = "Pathumthani, Thailand",
MONTH = "December",
YEAR = 1995,
PUBLISHER = "Springer-Verlag, LNCS 1023",
PAGES = "301--318",
ABSTRACT = {
We present a methodology for logic program development based on the use of
verified transformation templates. We use the Isabelle Logical Framework to
formalize transformation templates as inference rules. We derive these rules
in higher-order logic and afterwards use higher-order unification to apply them to develop programs in a deductive synthesis style. Our work addresses the
pragmatics of template formalization and application as well as which
theories and semantics of programs and data we require to derive templates. 
}
}