pdfreaders.org

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.

Keywords:
Categories:
Documents:

QR Code for talk:brucker:encoding:2010.Please cite this article as follows:
Achim D. Brucker. Encoding Object-oriented Datatypes in HOL: Extensible Records Revisited. Isabelle Developers Workshop (IDW), Cambridge, UK, 28. jun. 2010.
(slides) (handout) (BibTeX) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@Talk{ talk:brucker:encoding:2010,
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.},
address = {Cambridge, UK},
author = {Achim D. Brucker},
day = {28},
event = {Isabelle Developers Workshop (IDW)},
handout = {https://www.brucker.ch/bibliography/download/2010/talk-brucker-encoding-2010-2x2.pdf},
isodate = {2010-06-18},
lecturer = {Achim D. Brucker},
month = {jun},
slides = {https://www.brucker.ch/bibliography/download/2010/talk-brucker-encoding-2010.pdf},
slideshare = {26244397},
slideshare_height = {356},
slideshare_width = {427},
title = {Encoding Object-oriented Datatypes in HOL: Extensible Records Revisited},
url = {https://www.brucker.ch/bibliography/abstract/talk-brucker-encoding-2010},
year = {2010},
}