@InCollection{	  brucker.ea:embedding:2003,
  abstract	= {Tools for a specification language can be implemented
		  \emph{directly} (by building a special purpose theorem
		  prover) or \emph{by a conservative embedding} into a typed
		  meta-logic, which allows their safe and logically
		  consistent implementation and the reuse of existing theorem
		  prover engines. For being useful, the conservative
		  extension approach must provide derivations for several
		  thousand ``folklore'' theorems. In this paper, we present
		  an approach for deriving the mass of these theorems
		  mechanically from an existing library of the meta-logic.
		  The approach presupposes a structured \emph{theory
		  morphism} mapping library datatypes and library functions
		  to new functions of the specification language while
		  uniformly modifying some semantic properties; for example,
		  new functions may have a different treatment of
		  undefinedness compared to old ones.},
  keywords	= {Formal Methods, Formal Semantics, Shallow Embeddings,
		  Theorem Proving, OCL},
  location	= {Nijmegen},
  author	= {Achim D. Brucker and Burkhart Wolff},
  booktitle	= {Types for Proof and Programs},
  language	= {USenglish},
  pages		= {59--77},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  series	= {Lecture Notes in Computer Science},
  number	= {2646},
  isbn		= {3-540-14031-X},
  editor	= {Herman Geuvers and Freek Wiedijk},
  pdf		= {http://www.brucker.ch/bibliography/download/2003/brucker.ea-embedding-2003.pdf},
  project	= {CSFMDOS},
  title		= {Using Theory Morphisms for Implementing Formal Methods
		  Tools},
  doi		= {10.1007/3-540-39185-1_4},
  issn		= {0302-9743},
  categories	= {holocl},
  classification= {workshop},
  areas		= {formal methods},
  year		= {2003},
  public	= {yes},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-embedding-2003}
		  
}