Inter-deriving Semantic Artifacts for Object-Oriented Programming

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  • Department of Computer Science
We present a new abstract machine for Abadi and Cardelli's untyped non-imperative calculus of objects.  This abstract machine mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (i.e., big-step operational semantics) specified in Abadi and Cardelli's monograph.  To move closer to actual implementations, which use environments rather than actual substitutions, we then represent methods as closures and we present three new semantic artifacts for a version of Abadi and Cardelli's calculus with explicit substitutions: a reduction semantics, an environment-based abstract machine, and a natural semantics (i.e., an interpreter) with environments.  These three new semantic artifacts mechanically correspond to each other, and the two abstract machines are bisimilar.  Their significance lies in the fact that they have not been designed from scratch and then proved correct; instead, they have been inter-derived.

To illustrate the inter-derivation and to make this article stand-alone, we also comprehensively treat the example of negational normalization over Boolean formulas, in appendix.


Original languageEnglish
JournalJournal of Computer and System Sciences
Volume76
Issue5
Pages (from-to)302-323
Number of pages22
ISSN0022-0000
DOIs
Publication statusPublished - 2010

Bibliographical note

Title of the special issue: Workshop on Logic, Language, Information and Computation / Edited by Wilfrid Hodges and Ruy de Queiroz

    Research areas

  • functional calculus of objects, reduction semantics, abstract machine, natural semantics, syntactic correspondence, functional correspondence

See relations at Aarhus University Citationformats

ID: 19071377