Prototyping SOS Meta-theory in Maude

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. Key words: Formal Semantics, Structural Operational Semantics, Term Rewriting, Language Prototyping, Maude.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Mohammad Reza Mousavi, Michel A. Reniers
• Keywords: ENTCS 2006, Maude Term, Prototype Implementation, Semantics