@Article{	  brucker.ea:extensible:2008-b,
  abstract	= {We present an extensible encoding of object-oriented data
		  models into HOL. Our encoding is supported by a datatype
		  package that leverages the use of the shallow embedding
		  technique to object-oriented specification and programming
		  languages. The package incrementally 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, and co-inductive class
		  invariants. The package is conservative, i.e., all
		  properties are derived entirely from constant definitions,
		  including the constraints over object structures. As an
		  application, we use the package for an object-oriented
		  core-language called IMP++, for which we formally prove the
		  correctness of a Hoare-Logic with respect to a denotational
		  semantics.},
  author	= {Achim D. Brucker and Burkhart Wolff},
  language	= {USenglish},
  public	= {yes},
  classification= {journal},
  areas		= {formal methods, software},
  keywords	= {object-oriented data models, HOL, theorem proving,
		  verification},
  title		= {An Extensible Encoding of Object-oriented Data Models in
		  HOL},
  year		= {2008},
  journal	= {Journal of Automated Reasoning},
  volume	= {41},
  issue		= {3},
  pages		= {219--249},
  issn		= {0168-7433},
  doi		= {10.1007/s10817-008-9108-3},
  categories	= {holocl},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  pdf		= {http://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008-b.pdf},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b}
		  
}