Encoding Object-oriented Datatypes in HOL: Extensible Records Revisited

By Achim D. Brucker.

We briefly present the theorem proving environment HOL-OCL. The HOL-OCL system is an interactive proof environment for object-oriented (i.e., UML/OCL) specifications that is build on top of Isabelle/HOL. Overall, we introduce the overall system architecture and, in more detail, our extensible encoding of object-oriented data models into HOL.

While our extensible encoding is inspired by the extensible record package of Isabelle/HOL, its implementation is not directly based on it. In this talk, we will discuss how our approach differs from the existing one and discuss how it serves as a basis for implementing allows for implementing Isabelle-based tools for object-oriented models.

Please cite this work as follows:
A. D. Brucker, “Encoding object-oriented datatypes in HOL: Extensible records revisited,” presented at the Isabelle developers workshop (IDW), Cambridge, UK, Jun. 18, 2010. Author copy: https://logicalhacking.com/publications/talk-brucker-encoding-2010/

BibTeX
@Unpublished{ talk:brucker:encoding:2010,
  date              = {2010-06-18},
  title             = {Encoding Object-oriented Datatypes in HOL: Extensible Records
                       Revisited},
  author            = {Achim D. Brucker},
  eventtitle        = {Isabelle Developers Workshop (IDW)},
  slideshare        = {26244397},
  slideshare_width  = {427},
  slideshare_height = {356},
  abstract          = {We briefly present the theorem proving environment HOL-OCL.
                       The HOL-OCL system is an interactive proof environment for
                       object-oriented (i.e., UML/OCL) specifications that is build
                       on top of Isabelle/HOL. Overall, we introduce the overall
                       system architecture and, in more detail, our extensible
                       encoding of object-oriented data models into HOL.
                       
                       While our extensible encoding is inspired by the extensible
                       record package of Isabelle/HOL, its implementation is not
                       directly based on it. In this talk, we will discuss how our
                       approach differs from the existing one and discuss how it
                       serves as a basis for implementing allows for implementing
                       Isabelle-based tools for object-oriented models.},
  venue             = {Cambridge, UK},
  areas             = {software, formal methods},
  note              = {Author copy: \url{https://logicalhacking.com/publications/talk-brucker-encoding-2010/}},
  pdf               = {https://logicalhacking.com/publications/talk-brucker-encoding-2010/talk-brucker-encoding-2010.pdf},
}