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 alpha-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.

Last modified: Sun Sep 11 18:06:01 MDT 2011