Prototyping SOS Meta-theory in Maude Export

@article{citeulike:875769, abstract = {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.}, author = {Mousavi, Mohammad R. and Reniers, Michel A.}, booktitle = {Proceedings of the Second Workshop on Structural Operational Semantics (SOS 2005)}, citeulike-article-id = {875769}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.entcs.2005.09.030}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B75H1-4JXS6XG-8/2/cda60ec4c0a8eec26310c2b364f67a80}, day = {15}, doi = {10.1016/j.entcs.2005.09.030}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {maude, operationalsemantics}, month = {May}, number = {1}, pages = {135--150}, posted-at = {2008-02-13 16:21:11}, priority = {2}, publisher = {Elsevier}, title = {Prototyping SOS Meta-theory in Maude}, url = {http://dx.doi.org/10.1016/j.entcs.2005.09.030}, volume = {156}, year = {2006} }

TY - JOUR ID - citeulike:875769 L3 - citeulike-article-id:875769 N2 - 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. IS - 1 JF - Electronic Notes in Theoretical Computer Science EP - 150 TI - Prototyping SOS Meta-theory in Maude PB - Elsevier VL - 156 T2 - Proceedings of the Second Workshop on Structural Operational Semantics (SOS 2005) SP - 135 KW - maude KW - operationalsemantics AU - Mousavi, Mohammad AU - Reniers, Michel PY - 2006/05/15/ UR - http://dx.doi.org/10.1016/j.entcs.2005.09.030 ER -