Extensible Transition System Semantics

Casper Bach Poulsen


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: