Sciweavers

TPHOL
1998
IEEE

Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic

13 years 7 months ago
Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic
We show how extensible records with structural subtyping can be represented directly in Higher-Order Logic (HOL). Exploiting some specific properties of HOL, this encoding turns out to be extremely simple. In particular, structural subtyping is subsumed by naive parametric polymorphism, while overridable generic functions may be based on overloading. Taking HOL plus extensible records as a starting point, we then set out to build an environment for object-oriented specification and verification (HOOL). This framework offers several well-known concepts like classes, objects, methods and late-binding. All of this is achieved by very simple means within HOL.
Wolfgang Naraschewski, Markus Wenzel
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where TPHOL
Authors Wolfgang Naraschewski, Markus Wenzel
Comments (0)