A Metalanguage for Structural Operational Semantics (Abstract)

This paper introduces MLSOS, a functional metalanguage for declaring and animating definitions of structural operational semantics. The language provides a general mechanism for resolution-based search that respects the α-equivalence of object-language binding structures, based on nominal unification. It combines that with a FreshML-style generative treatment of bound names. We claim that MLSOS allows animation of operational semantics definitions to be prototyped in a natural way, starting from semi-formal specifications. We outline the main design choices behind the language and illustrate its use.