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