@Article{	  brucker.ea:extensible:2008,
  abstract	= {We present an extensible encoding of object-oriented data
		  models into higher-order logic (HOL). Our encoding is
		  supported by a datatype package that leverages the use
		  ofthe shallow embedding technique to
		  object-orientedspecification and programming languages. The
		  packageincrementally compiles an object-oriented data
		  model, i.e.,a class model, to a theory containing
		  object-universes,constructors, accessor functions,
		  coercions (casts) between dynamic and static types,
		  characteristic sets, andco-inductive class invariants. The
		  package is conservative,i. e., all properties are derived
		  entirely from constantdefinitions, including the
		  constraints over objectstructures. As an application, we
		  use the package for anobject-oriented core-language called
		  IMP++, for which weformally prove the correctness of a
		  Hoare logic withrespect to a denotational semantics.},
  author	= {Achim D. Brucker and Burkhart Wolff},
  journal	= {Journal of Automated Reasoning (JAR)},
  language	= {USenglish},
  note		= {Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias
		  Nipkow (eds)},
  number	= {3-4},
  pages		= {219--249},
  pdf		= {papers/2008/pre-fac-datatype.pdf},
  title		= {An Extensible Encoding of Object-oriented Data Models in
		  HOL with an Application to IMP++},
  url		= {http://dx.doi.org/10.1007/s10817-008-9108-3},
  volume	= {Selected Papers of the AVOCS-VERIFY Workshop 2006},
  year		= 2008,
  user		= {lukasbru}
}