Seperation Logic

Context. The object calculi of Abadi and Cardelli provide idealized models of object-oriented
programming languages [1]. They have rigorously defined semantics, and they are simple since
only objects are considered as primitives. At the same time they are expressive enough to encode
all common features of practical (i.e., class-based) object-oriented programming languages
like classes, subtyping and inheritance. In this work we will study the semantics of a variant of
Abadi and Cardelli’s imperative object calculus, as presented by Abadi and Leino [2]. This calculus
is particularly interesting since it combines objects with dynamically allocated, higher-order
store.
While higher-order store is present in di_erent forms in almost all practical programming
languages (pointers to functions in C, callbacks in Java, or general references in ML), it is challenging
to find good semantic models in which one can reason about the behaviour of programs.
Syntactic arguments, based solely on the operational semantics, su_ce to prove properties such
as type preservation, but are not suitable as a basis for program logics like that of Abadi and
Leino [2]. We believe that specifications of program behaviour should have a meaning independent
of the particular proof system on which syntactic preservation proofs rely [7, 6, 10]. On the
other hand, a "classical" denotational semantics of higher-order store based on partial orders
tends to become rather complex. In fact, modelling dynamic allocation alone usually means
that one has to move to a possible-world model, formalized as a category of functors over cpos.
While this achieves the goal of separating the notion of logical validity from derivability, the
known models are not very abstract in that many natural equivalences involving state do not
hold.
An alternative is to use a step-indexed semantics, an approach developed by Appel and his
collaborators in the context of foundational proof-carrying code [5]. Based on a small-step operational
semantics, types are interpreted as sets of indexed values. Informally, an expression has
a certain type if it behaves like an element of that type for a fixed number of steps. The usual
type inference rules then become derived lemmas, and type safety of the operational semantics
is an immediate consequence of this interpretation of types.
A step-indexed semantics has been introduced for lambda calculus with recursive and polymorphic
types in [5]. Later this has been successfully extended to an imperative language with
general references and impredicative polymorphism [3], substructural state [4], and has also
been used for low-level languages [5, 7].
Task description. The aim of this thesis is to develop a step-indexed semantics for the imperative
object calculus. The main goal is to define such a semantics for simple object types,
and prove the usual type inference rules sound. Once this has been achieved, there are several
extensions of the construction that can be investigated:
• Enriching the type system with features such as subtyping, recursive object types or impredicative
polymorphism.
• Defining a program logic for the imperative object calculus, along the lines of [2]. The
logic may then even be adapted to local and modular reasoning in the style of separation
logic [9, 8].