A Metalanguage for Structural Operational Semantics.
Matthew R. Lakin, Andrew M. Pitts · 2007
We present MLSOS, a functional metalanguage for encoding definitions of structural operational semantics. The key features of this language are inbuilt support for representing object-language binding structures and performing proof-search. MLSOS uses the nominal approach to dealing with binders and a FreshML-style generative treatment of atoms. This allows us to prototype systems in a natural way, starting from a semi-formal specification. We outline the main design choices behind the language and illustrate its use. 1