We present a prototype implementation of SOS meta-theory in the Maude term rewriting language. The prototype defines the basic concepts of SOS meta-theory (e.g., transition formulae, deduction rules and transition system specifications) in Maude. Besides the basic definitions, we implement methods for checking the premises of some SOS meta-theorems (e.g., GSOS congruence meta-theorem) in this framework. Furthermore, we define a generic strategy for animating programs and models for semantic specifications in our meta-language. The general goal of this line of research is to develop a general-purpose tool that assists language designers by checking useful properties about the language under definition and by providing a rapid prototyping environment for scrutinizing the actual behavior of programs according to the defined semantics.
|Title of host publication||Proceedings of the 2nd Workshop on Structural Operational Semantics (SOS2005, Lisbon, Portugal, July 10, 2005; satellite to ICALP2005)|
|Editors||P.D. Mosses, I. Ulidowski|
|Publication status||Published - 2006|
|Name||Electronic Notes in Theoretical Computer Science|