Aarhus University Seal / Aarhus Universitets segl

Danish

You are here: AU » About Aarhus University » Organisation » Inter-deriving Semantic Artifacts for Object-Oriented Pro...

About Aarhus University

Inter-deriving Semantic Artifacts for Object-Oriented Programming

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

Standard

Inter-deriving Semantic Artifacts for Object-Oriented Programming. / Danvy, Olivier; Johannsen, Jacob.

In: Journal of Computer and System Sciences, Vol. 76, No. 5, 2010, p. 302-323.

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

Harvard

Danvy, O & Johannsen, J 2010, 'Inter-deriving Semantic Artifacts for Object-Oriented Programming', Journal of Computer and System Sciences, vol. 76, no. 5, pp. 302-323. https://doi.org/10.1016/j.jcss.2009.10.004

APA

Danvy, O., & Johannsen, J. (2010). Inter-deriving Semantic Artifacts for Object-Oriented Programming. Journal of Computer and System Sciences, 76(5), 302-323. https://doi.org/10.1016/j.jcss.2009.10.004

CBE

Danvy O, Johannsen J. 2010. Inter-deriving Semantic Artifacts for Object-Oriented Programming. Journal of Computer and System Sciences. 76(5):302-323. https://doi.org/10.1016/j.jcss.2009.10.004

MLA

Danvy, Olivier and Jacob Johannsen. "Inter-deriving Semantic Artifacts for Object-Oriented Programming". Journal of Computer and System Sciences. 2010, 76(5). 302-323. https://doi.org/10.1016/j.jcss.2009.10.004

Vancouver

Danvy O, Johannsen J. Inter-deriving Semantic Artifacts for Object-Oriented Programming. Journal of Computer and System Sciences. 2010;76(5):302-323. https://doi.org/10.1016/j.jcss.2009.10.004

Author

Danvy, Olivier ; Johannsen, Jacob. / Inter-deriving Semantic Artifacts for Object-Oriented Programming. In: Journal of Computer and System Sciences. 2010 ; Vol. 76, No. 5. pp. 302-323.

Bibtex

@article{354f4880125611dfb95d000ea68e967b,
title = "Inter-deriving Semantic Artifacts for Object-Oriented Programming",
abstract = "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.",
keywords = "functional calculus of objects, reduction semantics, abstract machine, natural semantics, syntactic correspondence, functional correspondence",
author = "Olivier Danvy and Jacob Johannsen",
note = "Title of the special issue: Workshop on Logic, Language, Information and Computation / Edited by Wilfrid Hodges and Ruy de Queiroz",
year = "2010",
doi = "10.1016/j.jcss.2009.10.004",
language = "English",
volume = "76",
pages = "302--323",
journal = "Journal of Computer and System Sciences",
issn = "0022-0000",
publisher = "Academic Press",
number = "5",

}

RIS

TY - JOUR

T1 - Inter-deriving Semantic Artifacts for Object-Oriented Programming

AU - Danvy, Olivier

AU - Johannsen, Jacob

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

PY - 2010

Y1 - 2010

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

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

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

U2 - 10.1016/j.jcss.2009.10.004

DO - 10.1016/j.jcss.2009.10.004

M3 - Journal article

VL - 76

SP - 302

EP - 323

JO - Journal of Computer and System Sciences

JF - Journal of Computer and System Sciences

SN - 0022-0000

IS - 5

ER -