@InCollection{	  brucker.ea:extensible:2008,
  abstract	= {We present a datatype package that enables the shallow
		  embedding technique to object-oriented specification and
		  programming languages. The package incrementally compiles
		  an object-oriented data model to a theory containing
		  object-universes, constructors, and accessors functions,
		  coercions between dynamic and static types, characteristic
		  sets, their relations reflecting inheritance, and the
		  necessary class invariants. The package is conservative,
		  i.e., all properties are derived entirely from axiomatic
		  definitions. As an application, we use the package for an
		  object-oriented core-language called IMP++, for which
		  correctness of a Hoare-Logic with respect to an operational
		  semantics is proven. },
  location	= {Paphos, Cyprus},
  author	= {Achim D. Brucker and Burkhart Wolff},
  booktitle	= {ECOOP 2008 -- Object-Oriented Programming},
  language	= {USenglish},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  series	= {Lecture Notes in Computer Science},
  doi		= {10.1007/978-3-540-70592-5_19},
  title		= {Extensible Universes for Object-oriented Data Models},
  categories	= {holocl},
  number	= {5142},
  pages		= {438--462},
  classification= {conference},
  areas		= {formal methods, software},
  keywords	= {object-oriented data models, HOL, formal methods, UML,
		  OCL},
  year		= {2008},
  editor	= {Jan Vitek},
  pdf		= {http://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008.pdf},
  public	= {yes},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008}
		  
}