Semantics and Logic of Object Calculi

Reus, Bernhard and Streicher, Thomas (2002) Semantics and Logic of Object Calculi. In: 17th Symposium on Logic in Computer Science, Copenhagen.

Full text not available from this repository.


The main contribution of this paper is a formal characterization of recursive object specifications based on a denotational untyped semantics of the object calculus and the discussion of existence of those (recursive) specifications. The semantics is then applied to prove soundness of a programming logic [2] for the object calculus [1] and to suggest possible extensions. For the purposes of this discussion we use an informal logic of predomains in order to avoid any commitment to a particular syntax of specification logic.

Item Type: Conference or Workshop Item (Paper)
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 denotatinal semanticsl; 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: accepted and cited by Abadi and Leino who have invented the first logic on objects. This is an extended abstract of a journal version that appeared in 2004 in Theoretical Computer Science. Outlet/citations: top theoretical computer science conference, long running (over 20 years), most important conference on logic in computer science; 26.7% acceptance rate, citations 9 (google scholar)
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Bernhard Reus
Date Deposited: 06 Feb 2012 20:35
Last Modified: 12 Apr 2012 11:14
📧 Request an update