TY  - CHAP
AU  - Brucker, Achim D.
AU  - Wolff, Burkhart
ED  - Geuvers, Herman
ED  - Wiedijk, Freek
PY  - 2003//
TI  - Using Theory Morphisms for Implementing Formal Methods Tools
BT  - Types for Proof and Programs
T3  - Lecture Notes in Computer Science
SP  - 59
EP  - 77
IS  - 2646
PB  - Springer-Verlag
CY  - Heidelberg
KW  - Formal Methods, Formal Semantics, Shallow Embeddings, Theorem Proving, OCL
N2  - Tools for a specification language can be implemented directly (by building a special purpose theorem prover) or 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 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.
SN  - 3-540-14031-X
UR  - http://www.brucker.ch/bibliography/abstract/brucker.ea-embedding-2003
L1  - http://www.brucker.ch/bibliography/download/2003/brucker.ea-embedding-2003.pdf
UR  - http://dx.doi.org/10.1007/3-540-39185-1_4
ID  - brucker.ea:embedding:2003
ER  -