Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 A Metalanguage for Structural Operational Semantics (Abstract)
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.