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.