MohammadReza Mousavi, Michel Reniers, Proceedings of the 2nd Workshop on Structural Operational Semantics (SOS'05), Lisbon, Portugal, Electronic Notes in Theoretical Computer Science, 156(1):135-150, Elsevier Science B.V., September 2005.
. 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.
Paper in .pdf format in .ps format Accompanying Code in Maude
@InProceedings{MousaviSOS05-01,
author = "Mousavi, MohammadReza and Reniers, Michel A.",
title = "Prototyping SOS Meta-theory in Maude",
booktitle = "Proceedings of the 2nd Workshop on Structural Operational Semantics (SOS'05)",
series = "Electronic Notes in Theoretical Computer Science",
address = "Lisboa, Portugal",
publisher = "Elsevier Science B.V.",
year = "2005"
}