[isabelle] Paper Available



Dear all,

we are happy to announce the following paper:

Authors: Achim D. Brucker and Burkhart Wolff

Title: An Extensible Encoding of Object-oriented Data Models in
		  HOL with an Application to IMP++

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 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.


Comments and discussions are welcome!


Best regards,

Achim & bu





Bibtex-Entry:
@ARTICLE{brucker.ea:extensible:2008,

  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)}, pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/0_brucker.ea-datatype-2007.pdf },
  title = {An Extensible Encoding of Object-oriented Data Models in
		  HOL with an Application to IMP++},
  volume = {Selected Papers of the AVOCS-VERIFY Workshop 2006},
  doi = {10.1007/s10817-008-9108-3},
  pages = {219-249},
  volume = 41,
  number = {3--4},
  year = 2008
}







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.