A Metalanguage for Structural Operational Semantics

This paper introduces MLSOS, a functional meta-language for declaring and animating definitions of structural operational semantics. The authors claim that MLSOS allows animation of operational semantics definitions to be prototyped in a natural way, starting from semi-formal specifications. They outline the main design choices behind the language and illustrate its use. There is currently a great deal of interest in (partially) automating various tasks in the field of programming language meta-theory. While there are many aspects to this research effort (see for a survey), the paper reported here focuses on animating definitions of type systems and operational semantics.