Extensible Transition System Semantics
Abstract
Structural operational semantics (SOS) come in two main styles: big-step and small-step. Each style has its merits and drawbacks, and it is sometimes useful to maintain specifications in both styles. But it is both tedious and error-prone to maintain multiple specifications of the same language. Additionally, big-step SOS has poor support for language evolution, requires reformulation or introduction of new rules for existing constructs as a language is extended, and is sometimes regarded as inferior for type soundness proofs. This thesis addresses pragmatic shortcomings with giving and relating extensible small-step and big-step specifications, and with big-step type soundness proofs.
The main contributions of this thesis are:
we present Extensible SOS (XSOS), a simple but novel extension of Mosses’ Modular SOS that supports concise and extensible specification of language features for both big-step and small-step semantics;
we internalise the well-known refocusing transformation in XSOS to provide a systematic transformation between extensible small-step and big-step specifications;
we consider types as abstract interpretations as a novel approach to big-step type soundness; and
we propose a novel type system for Hindley-Milner-Damas polymorphic type inference for a language with ML style references.