Maude

[Brian Rice]

Maude is a reflective language and system which supports both equations and
re-write logic for specification and programming.  Since re-writing logic
can naturally express state and concurrency, it can serve as a general
semantic framework for many languages as well as a meta-logic for many other
logics' execution.
Maude supports logical reflection, allowing for an extensible algebra of
module composition and advanced metaprogramming and metalinguistics.  It
provides environments for logics, theorem provers, and models of
computation.
Maude is available for free for a few Unix implementations, sans source
code, from here (http://maude.csl.sri.com/).