Modular Structural operational semantics (MSOS) is a way of writing language specifications using inference rules. The modularity focus in MSOS is on reusing inference rules when new effects are added to a language. In traditional SOS, if we define evaluation for an arithmetic language, we need to rewrite the rules to include an environment if we want to add variables. MSOS gives us a formal way to reuse the rules from the arithmetic language without modification.
In this example, we examine whether we can model in Sterling the same addition of effects to evaluation without modifying rules. We do this by threading around a context to which we may add new types of elements for new effects, such as an environment for a language including variables. Our language is based on the one in the MSOS paper. However, in the interests of examining different types of additions, we pare the host language back farther than in the paper, moving Booleans and constant declarations into extensions.
There are some parts of MSOS extensibility we cannot mimic. Because its modularity is focused on adding effects to existing evaluation relations, not on adding new syntax or semantic relations, it allows extensions to write new rules for evaluating existing constructs. In the paper language, this is used for adding errors in evaluation as a modular effect, defining error evaluation as part of an extension for host-language-introduced arithmetic expressions. Because of Sterling's focus on adding new syntax and semantic relations in extensions and ensuring the composed semantics are reasonable, we do not allow the introduction of such rules and thus cannot completely model MSOS.