
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/
@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},
}