This thesis is concerned with reasoning about stateful programs where storage of values of all types is possible, including those of higher type. This feature is often referred to as higher-order store; examples are the objects in the object calculus of Abadi and Cardelli as well as the general references of languages such as Standard ML and Scheme. Higher-order store introduces recursion ``through the store'' to the language, and requires the semantic domain to be defined by a mixed-variant recursive equation. Using domain-theoretic techniques we investigate semantics and logics of languages with higher-order store, with particular emphasis on object-oriented languages where subtyping introduces additional complexity.
The thesis is divided into three parts. The first one surveys some key technical results from domain theory, and summarises various proposals of semantic interpretations of both functional and imperative objects found in the literature. The object calculus that is considered throughout Parts II and III is presented, including its operational and denotational semantics.
Part II presents
a denotational semantics for Abadi and Leino's logic of objects. Our soundness proof provides an insightful alternative to the original proof of Abadi and Leino which was given with respect to an operational semantics. By separating validity from derivability in the proof system, we clarify the meaning of specifications of the logic. The logic is also extended by a notion of recursive specification and appropriate proof rules are introduced.
In the final part, the problem of finding a typed model of the object calculus is addressed. Starting from a model of an ML-like language recently presented by Levy, we add subtyping to obtain a semantic model that is sufficiently rich to interpret imperative objects.
The semantics is presented as a possible worlds model that explicates the allocation of new memory; subtyping is interpreted using coercion maps.
After establishing coherence by extending a method due to Reynolds, a number of non-trivial programs are shown to meet their specifications.