Semantics and logic of object calculi

Reus, Bernhard and Streicher, Thomas (2004) Semantics and logic of object calculi. Theoretical Computer Science, 316 (1-3). pp. 191-213. ISSN 0304-3975

Full text not available from this repository.


The main contribution of this paper is a formal characterization of recursive object specifications and their existence based on a denotational untyped semantics of the object calculus. Existence is not guaranteed but can be shown employing Pitts’ results on relational properties of domains. The semantics can be used to analyse and verify Abadi and Leino's object logic but it also suggests extensions. For example, specifications of methods may not only refer to fields but also to methods of objects in the store. This can be achieved without compromising the existence theorem. An informal logic of predomains is in use intentionally in order to avoid any commitment to a particular syntax of specification logic.

Item Type: Article
Additional Information: Originality: new semantical view on objects and reasoning principles on objects in object-oriented languages (specifically ones where objects can have their own method suites) Rigour: uses denotational semantics; full mathematical model and proof using existence of recursive predicates and results from domain theory. Significance: first use of this technique to prove logics for objects, potential blueprint for correctness proofs of similar logics. Impact: positively acknowledged and cited by Abadi & Leino who have invented the first logic on objects. This TCS paper is the long version of an extended abstract by Reus&Streicher which appeared in 2002 in LICS, the top logic in computer science conference (long running > 20 years) with a 26% acceptance rate in that year. Citations: 9 (google scholar)
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Bernhard Reus
Date Deposited: 06 Feb 2012 19:10
Last Modified: 24 Sep 2019 11:29
📧 Request an update