@TechReport{	  it:2003-008,
  author	= {Julian Richardson and Pierre Flener},
  title		= {Program Schemas as Proof Methods},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Computing Science Division},
  year		= {2003},
  number	= {2003-008},
  month		= feb,
  abstract	= {Automatic proof and automatic programming have always
		  enjoyed a close relationship. We present a unification of
		  proof planning (a knowledge-based approach to automated
		  proof) and schema-guided synthesis (a knowledge-based
		  approach to automatic programming). This unification
		  enhances schema-guided synthesis with features of proof
		  planning, such as the use of heuristics and the separation
		  between object-level and meta-level reasoning. It enhances
		  proof planning with features of schema-guided synthesis,
		  such as reuse. It allows program schemas and heuristics to
		  be implemented as proof planning methods. We aim
		  particularly at implementation within the lambda-Clam proof
		  planner, whose higher-order features are particularly
		  appropriate for synthesis. Program synthesis and
		  satisfaction of its proof obligations, such as verification
		  conditions, matchings, or simplifications, are thus neatly
		  integrated.}
}