Semantics and Logic of Object Calculi

Bernhard Reus and Thomas Streicher

To appear at Symposium on Logic in Computer Science (LICS'2002), Copenhagen, Denmark, July 22nd - 25th, 2002


The main contribution of this paper is a formal characterization of recursive object specifications based on a denotational untyped semantics of Abadi & Cardelli's object calculus and the discussion of existence of those (recursive) specifications. The existence theorem uses domain theoretical machinery known from the work of Freyd and Pitts. The semantics is then applied to prove soundness of a programming logic for the object calculus (by Abadi & Leino) 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 special syntax of specification logic

Server START Conference Manager
Update Time 15 Mar 2002 at 15:30:30
Start Conference Manager
Conference Systems