|
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., |
