Nordic Journal of Computing Bibliography

K. Rustan M. Leino. Recursive Object Types in a Logic of Object-Oriented Programs. Nordic Journal of Computing, 5(4):330-360, Winter 1998.

This paper formalizes a small object-oriented programming notation. The notation features imperative commands where objects can be shared (aliased), and is rich enough to allow subtypes and recursive object types. The syntax, type checking rules, axiomatic semantics, and operational semantics of the notation are given. A soundness theorem showing the consistency between the axiomatic and operational semantics is stated and proved. A simple corollary of the soundness theorem demonstrates the soundness of the type system. Because of the way types, fields, and methods are declared, no extra effort is required to handle recursive object types.

Categories and Subject Descriptors: D.3 [Programming Languages]; D.3.1 [Programming Languages]: Formal Definitions and Theory

Additional Key Words and Phrases: programming logic, object-oriented programs, recursive object types, program correctness, axiomatic semantics, soundness

Selected references


  • Nordic Journal of Computing homepage
  • Bibliography top level
  • Nordic Journal of Computing Author Index
  • Search the HBP database