@InCollection{ brucker.ea:using: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.}, address = {Nijmegen}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Types 2002, Proceedings of the workshop Types for Proof and Programs}, copyright = {\copyright Springer-Verlag}, copyrighturl = {http://link.springer-ny.com/link/service/series/0558/}, editor = {Herman Geuvers and Freek Wiedijk}, isbn = {3-540-14031-X}, language = {USenglish}, publisher = {Springer-Verlag}, series = {LNCS 2646.}, title = {Using Theory Morphisms for Implementing Formal Methods Tools}, year = 2003, user = {wolff} }