From operational semantics to abstract machines

Research output: Contribution to journalArticlepeer-review

50 Scopus citations


We consider the problem of mechanically constructing abstract machines from operational semantics, producing intermediate-level specifications of evaluators guaranteed to be correct with respect to the operational semantics. We construct these machines by repeatedly applying correctness-preserving transformations to operational semantics until the resulting specifications have the form of abstract machines. Though not automatable in general, this approach to constructing machine implementations can be mechanized, providing machine-verified correctness proofs. As examples, we present the transformation of specifications for both call-by-name and call-by-value evaluation of the untyped 2-calculus into abstract machines that implement such evaluation strategies. We also present extensions to the call-by-value machine for a language containing constructs for recursion, conditionals, concrete data types, and built-in functions. In all cases, the correctness of the derived abstract machines follows from the (generally transparent) correctness of the initial operational semantic specification and the correctness of the transformations applied.

Original languageEnglish (US)
Pages (from-to)415-459
Number of pages45
JournalMathematical Structures in Computer Science
Issue number4
StatePublished - Dec 1992

All Science Journal Classification (ASJC) codes

  • Mathematics (miscellaneous)
  • Computer Science Applications


Dive into the research topics of 'From operational semantics to abstract machines'. Together they form a unique fingerprint.

Cite this