Paper: Semantics and Logic of Object Calculi (at LICS 2002)

Authors: Bernhard Reus Thomas Streicher

Abstract

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

BibTeX

  @InProceedings{ReusStreicher-SemanticsandLogicof,
    author = 	 {Bernhard Reus and Thomas Streicher},
    title = 	 {Semantics and Logic of Object Calculi},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS 2002)},
    year =	 {2002},
    month =	 {July}, 
    pages =      {113--122},
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }