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.
%0 Journal Article
%1 mousavi_06_prototyping
%A Mousavi, Mohammad R.
%A Reniers, Michel A.
%B Proceedings of the Second Workshop on Structural Operational Semantics (SOS 2005)
%D 2006
%I Elsevier
%J Electronic Notes in Theoretical Computer Science
%K 2006 maude sos
%N 1
%P 135--150
%R 10.1016/j.entcs.2005.09.030
%T Prototyping SOS Meta-theory in Maude
%U http://dx.doi.org/10.1016/j.entcs.2005.09.030
%V 156
%X 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.
@article{mousavi_06_prototyping,
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.},
added-at = {2009-02-11T20:58:18.000+0100},
author = {Mousavi, Mohammad R. and Reniers, Michel A.},
biburl = {https://www.bibsonomy.org/bibtex/28f654550b895c0dc4ac2a0f2433eaed0/leonardo},
booktitle = {Proceedings of the Second Workshop on Structural Operational Semantics (SOS 2005)},
citeulike-article-id = {875769},
doi = {10.1016/j.entcs.2005.09.030},
interhash = {0c2eab3ce15079f181941888dbaa7b90},
intrahash = {8f654550b895c0dc4ac2a0f2433eaed0},
journal = {Electronic Notes in Theoretical Computer Science},
keywords = {2006 maude sos},
month = May,
number = 1,
pages = {135--150},
posted-at = {2006-09-27 19:07:59},
priority = {2},
publisher = {Elsevier},
timestamp = {2009-02-11T20:58:18.000+0100},
title = {Prototyping SOS Meta-theory in Maude},
url = {http://dx.doi.org/10.1016/j.entcs.2005.09.030},
volume = 156,
year = 2006
}