@InCollection{	  meyer.ea:tactic-based:2005,
  abstract	= {Within a framework of correct code-generation from
		  HOLspecifications, we present a particular instance
		  concerned with the optimized compilation of a lazy language
		  (called MiniHaskell) to a strict language (called MiniML).
		  Both languages are defined as shallow embeddings into
		  denotational semantics based on Scott s cpo s, leading to a
		  derivation of the corresponding operational semantics in
		  order to cross-check the basic definitions. On this basis,
		  translation rules from one language to the other were
		  formally derived in Isabelle/HOL. Particular emphasis is
		  put on the optimized compilation of function applications
		  leading to the side-calculi inferring e.g. strictness of
		  functions. The derived rules were grouped and set-up as an
		  instance of our generic, tactic-based translator for
		  specifications to code.},
  author	= {Thomas Meyer and Burkhart Wolff},
  booktitle	= {Types for Proofs and Programs (TYPES 2004)},
  copyright	= {\copyright Springer-Verlag},
  copyrighturl	= {{http://dx.doi.org/10.1007/11617990_13}},
  editor	= {Jean-Christophe Filliatre and Christine Paulin and
		  Benjamin Werner},
  language	= {USenglish},
  month		= 8,
  pages		= {202--215},
  pdf		= {papers/2005/2_optcom.pdf},
  publisher	= {Springer Verlag},
  series	= {LNCS 3839},
  title		= {Tactic-based Optimized Compilation of Functional
		  Programs},
  year		= 2005,
  user		= {wolff}
}