Details

Autor(en) / Beteiligte

• Schwinghammer, J

Titel

Reasoning about denotations of recursive objects

Ort / Verlag

ProQuest Dissertations & Theses

Erscheinungsjahr

2006

Quelle

ProQuest Dissertations & Theses A&I

Beschreibungen/Notizen

• 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.