Prototyping SOS meta-theory in Maude

M.R. Mousavi, M.A. Reniers

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

9 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationProceedings of the 2nd Workshop on Structural Operational Semantics (SOS2005, Lisbon, Portugal, July 10, 2005; satellite to ICALP2005)
EditorsP.D. Mosses, I. Ulidowski
Publication statusPublished - 2006

Publication series

NameElectronic Notes in Theoretical Computer Science
ISSN (Print)1571-0061


Dive into the research topics of 'Prototyping SOS meta-theory in Maude'. Together they form a unique fingerprint.

Cite this