From operational semantics to abstract machines. Preliminary results

John Hannan, Dale Miller

Research output: Chapter in Book/Report/Conference proceedingConference contribution

19 Scopus citations


The operational semantics of functional programming languages is frequently presented using inference rules within simple metalogics. Such presentations of semantics can be high-level and perspicuous since meta-logics often handle numerous syntactic details in a declarative fashion. This is particularly true of the meta-logic we consider here, which includes simply typed λ-terms, quantification at higher types, and β-conversion. Evaluation of functional programming languages is also often presented using low-level descriptions based on abstract machines: simple term rewriting systems in which few high-level features are present. In this paper, we illustrate how a high-level description of evaluation using inference rules can be systematically transformed into a low-level abstract machine by removing dependencies on high-level features of the metalogic until the resulting inference rules are so simple that they can be immediately identified as specifying an abstract machine. In particular, we present in detail the transformation of two inference rules specifying call-by-name evaluation of the untyped λ-calculus into the Krivine machine, a stack-based abstract machine that implements such evaluation. The initial specification uses the meta-logic's β-conversion to perform substitutions. The resulting machine uses de Bruijn numerals and closures instead of formal substitution. We also comment on a similar construction of a simplified SECD machine implementing call-by-value evaluation. This approach to abstract machine construction provides a semantics-directed method for motivating, proving correct, and extending such abstract machines.

Original languageEnglish (US)
Title of host publicationProc 1990 ACM Conf LISP Funct Program
PublisherPubl by ACM
Number of pages10
ISBN (Print)089791368X, 9780897913683
StatePublished - 1990
EventProceedings of the 1990 ACM Conference on LISP and Functional Programming - Nice, Fr
Duration: Jun 27 1990Jun 29 1990

Publication series

NameProc 1990 ACM Conf LISP Funct Program


OtherProceedings of the 1990 ACM Conference on LISP and Functional Programming
CityNice, Fr

All Science Journal Classification (ASJC) codes

  • Engineering(all)
  • Software
  • Modeling and Simulation
  • Computational Theory and Mathematics
  • Computational Mathematics


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

Cite this