Inheritance in higher order logic: Modeling and reasoning

DOI10.1007/3-540-44659-1_19MaRDI QIDQ2754051zbMATH OpenFDO

Authors Marieke Huisman, Bart Jacobs

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2066/18842

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• A syntax-directed Hoare logic for object-oriented programming concepts.
• A proof outline logic for object-oriented programming
• Object-oriented verification based on record subtyping in higher-order logic
• Separation logic, abstraction and inheritance
• Inheritance of temporal logic properties.

Cited in

(15)

• An extensible encoding of object-oriented data models in HOL. With an application to IMP++
• Coalgebras and monads in the semantics of Java
• Verified software units
• Modeling inheritance as coercion in a symbolic computation system
• Separation logic, abstraction and inheritance
• scientific article; zbMATH DE number 43242 (Why is no real title available?)
• Object-oriented verification based on record subtyping in higher-order logic
• A Set-Theoretical Approach for the Induction of Inheritance Hierarchies
• Theoretical Aspects of Computing – ICTAC 2005
• Higher order programming in Java: introspection, subsumption and extraction
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• The HOL-CSP Refinement Toolkit
• HOL-CSP Version 2.0
• A Sound Type System for Physical Quantities, Units, and Measurements
• Towards verification of C\(\#\) programs: a three-level approach

Describes a project that uses

Uses Software

• Isabelle
• PVS

This page was built for publication: Inheritance in higher order logic: Modeling and reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2754051)