We present a general method to achieve modularity of semantic denitions of programming languages specied as rewrite theories. This provides both a modular alternative to SOS definitions - with good executability and formal analysis capabilities - and a systematic way to execute and analyze SOS denitions by translation. The relationship to Mosses' modular operational semantics (MSOS) is explored in detail, yielding a semantics-preserving translation that supports execution and formal analysis of MSOS specications in Maude.
(BibTeX entry) (gzip'ed Postscript)