@InProceedings{	  meyer.ea:correct:2000,
  author	= {T. Meyer and Burkhart Wolff},
  title		= {Correct Code-Generation in a Generic Framework},
  editor	= {M. Aargaard and J. Harrison and T. Schubert},
  classification= {proceedings},
  booktitle	= {TPHOLs 2000: Supplemental Proceedings},
  year		= 2000,
  series	= {OGI Technical Report CSE 00-009},
  pages		= {213--230},
  month		= jul,
  organization	= {Oregon Graduate Institute, Portland, USA},
  ps		= {papers/2000/CodeGen.ps.gz},
  pdf		= {papers/2000/CodeGen.pdf},
  language	= {USenglish},
  abstract	= {One major motivation for theorem provers is the
		  development of verified programs. In particular, synthesis
		  or transformational development techniques aim at a
		  formalised conversion of the original specification to a
		  final formula meeting some notion of executability. We
		  present a framework to describe such notions, a method to
		  formally investigate them and instantiate it for three
		  executable languages, based on three different forms of
		  recursion (two denotational and one based on well-founded
		  recursion) and develop their theory in Isabelle/HOL. These
		  theories serve as a semantic interface for a generic
		  code-generator which is set up for each program notion with
		  an individual code-scheme for SML.}
}

@InProceedings{	  meyer.ea:correct:2000,
  author	= {T. Meyer and Burkhart Wolff},
  title		= {Correct Code-Generation in a Generic Framework},
  editor	= {M. Aargaard and J. Harrison and T. Schubert},
  booktitle	= {TPHOLs 2000: Supplemental Proceedings},
  year		= 2000,
  series	= {OGI Technical Report CSE 00-009},
  classification= {proceedings},
  pages		= {213--230},
  month		= jul,
  organization	= {Oregon Graduate Institute, Portland, USA},
  ps		= {papers/2000/CodeGen.ps.gz},
  pdf		= {papers/2000/CodeGen.pdf},
  language	= {USenglish},
  abstract	= {One major motivation for theorem provers is the
		  development of verified programs. In particular, synthesis
		  or transformational development techniques aim at a
		  formalised conversion of the original specification to a
		  final formula meeting some notion of executability. We
		  present a framework to describe such notions, a method to
		  formally investigate them and instantiate it for three
		  executable languages, based on three different forms of
		  recursion (two denotational and one based on well-founded
		  recursion) and develop their theory in Isabelle/HOL. These
		  theories serve as a semantic interface for a generic
		  code-generator which is set up for each program notion with
		  an individual code-scheme for SML.}
}