By L. Thomas van Binsbergen, Neil Sculthorpe, Adrian Johnstone and Elizabeth Scott

Abstract

Structural Operational Semantics (SOS) is a well-established framework for specifying the semantics of programming languages. Implicitly Modular SOS (I-MSOS) is a variant of SOS that has recently been used as the basis for several formal specification languages, including CBS and DynSem. These specification languages are intended to be executable: it should be possible to generate a reference interpreter for a programming language from the inference rules that specify its semantics.

The topic of this paper is the efficient implementation of I-MSOS rules. Our approach is to compile I-MSOS rules from different specification languages to a common intermediate language (IML). IML is a lower level language, designed to facilitate refactoring and optimisation. Sets of IML rules can then be compiled to produce a reference interpreter for the programming language specified by the original I-MSOS rules.

In this paper we motivate and present IML, together with a reference interpreter for IML itself. We also define a compilation scheme from declarative I-MSOS rules to IML, and discuss the key optimisations IML supports.

Accompanying material

The archive below accompanies a revised version of a paper presented at the 28th symposium on Implementation and Application of Functional Languages.

IMSOS-IML.tar.gz (updated 07/12/2016)