@InCollection{	  brucker.ea:package:2006,
  author	= {Achim D. Brucker and Burkhart Wolff},
  title		= {A Package for Extensible Object-Oriented Data Models with
		  an Application to IMP++},
  editor	= {Abhik Roychoudhury and Zijiang Yang},
  booktitle	= {International Workshop on Software Verification and
		  Validation (SVV 2006)},
  year		= 2006,
  series	= {Computing Research Repository (CoRR)},
  month		= aug,
  address	= {Seattle, USA},
  language	= {USenglish},
  abstract	= {We present a datatype package that enables the use of
		  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
		  accessor 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
		  \IMPOO, for which correctness of a Hoare logic with respect
		  to an operational semantics is proven.},
  categories	= {holocl},
  ps		= {http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.ps.gz}
		  ,
  pdf		= {http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.pdf}
		  ,
  classification= {workshop},
  keywords	= {datatype package, extensible object-oriented data model,
		  object-oriented specification,shallow embedding}
}