The interpretation and inter-derivation of small-step and big-step specifications

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandling


  • Ian Zerny, Danmark
We study the interpretation and inter-derivation of big-step and small-step
specifications. In particular, we consider formal specifications of programming
languages, e.g., denotational semantics and operational semantics, and
investigate how these specifications relate to each other. We carry out this
investigation by interpreting specifications as programs in a pure functional
meta-language and by constructively deriving one program from the other using
program transformations. To this end, we use two derivational correspondences:
The functional correspondence between compositional higher-order
specifications and first-order transition systems, and the syntactic correspondence
between rewriting specifications and first-order transition systems.
The main contribution of this dissertation is threefold: First, we extend these
correspondences to systematically derive small-step reduction semantics and
abstract machines from big-step reduction strategies. Second, we show how
these correspondences can be used to relate specifications for lazy evaluation,
e.g., graph reduction and call-by-need evaluation. Third, we describe
an alternative interpretation of specifications as logic programs in a logical
framework, and we give a logical counterpart to the functional correspondence.
ForlagDepartment of Computer Science, University of Aarhus
Antal sider278
StatusUdgivet - 2014

Note vedr. afhandling

Supervisor: Olivier Danvy

Se relationer på Aarhus Universitet Citationsformater


Ingen data tilgængelig

ID: 54605731