Tool for specifying operational semantics for given formally specified programming language I am trying to translate code from one programming language into another (to be specific - from RuleML to Drools, but other pairs can be expected as well) and it would be nice to know - whether there exists more general workbenches for this. 

E.g. one can formally specify programming language, that is clear. But are there any tools that can be used for capturing the formal semantics for formally specified language. It is obvious that the operational semantics is the most suitable for industrial programming languages. And - if semantics is specified then the translation from one programming language into other can be done at the meta-level. I guess, that this maybe too hard for C-to-Java translation, but it should work for more modest, recent languages that are created by academia.

I have heard about Maude, but I guess that there can be something more. My experience is that Google can not replace bibliographies or suggestions from community. Thanks.
We have been working on one for the last few years: Lem, a higher-order, typed language with backends for OCaml, Coq, Isabelle/HOL, HOL4, LaTeX and HTML.  Lem has been used internally in the group to formalise various machine models (PowerPC, ARM, and so on), memory models (the C memory model, etc.), programming language semantics (OCaml Light), and so on.