@Article{	  ayari.ea:higher-order:2001,
  abstract	= {The Deductive Tableau of Manna and Waldinger is a formal
		  system withan associated methodology for synthesizing
		  functional programs byexistence proofs in classical
		  first-order theories. We reinterpretthe formal system in a
		  setting that is higher-order in two respects:higher-order
		  logic is used to formalize a theory of functionalprograms
		  and higher-order resolution is used to synthesize
		  programsduring proof. Their synthesis methodology can be
		  applied in oursetting as well as new methodologies that
		  take advantage of thesehigher-order features.The
		  reinterpretation gives us a framework for directly
		  formalizingand implementing the Deductive Tableau system in
		  standard theoremprovers that support the kinds of
		  higher-order reasoning listedabove. We demonstrate this, as
		  well as a new developmentmethodology, within a conservative
		  extension of higher-order logicin the Isabelle system. We
		  report too on a case-study in synthesizingsorting
		  programs.},
  author	= {Abdelwaheb Ayari and David Basin},
  journal	= {Journal of Symbolic Computation},
  language	= {USenglish},
  month		= {may},
  number	= 5,
  pages		= {487--520},
  ps		= {papers/2001/dedtab.ps.gz},
  title		= {A Higher-order Interpretation of Deductive Tableau},
  volume	= 31,
  year		= 2001
}