Pragmatics of Modular SOS

Abstract

Modular SOS is a recently-developed variant of Plotkin's Structural Operational Semantics (SOS) framework. It has several pragmatic advantages over the original framework--the most significant being that rules specifying the semantics of individual language constructs can be given definitively, once and for all.

Modular SOS is being used for teaching operational semantics at the undergraduate level. For this purpose, the meta-notation for modular SOS rules has been made more user-friendly, and derivation of computations according to the rules is simulated using Prolog.

After giving an overview of the foundations of Modular SOS, this paper gives some illustrative examples of the use of the framework, and discusses various pragmatic aspects.