Lambda the Ultimate

The paper about the Tom language accepted at RTA 07 is available on the net. Here is the abstract:

We present the Tom language that extends Java with the purpose of providing high level constructs inspired by the rewriting community. Tom furnishes a bridge between a general purpose language and higher level specifications that use rewriting. This approach was motivated by the promotion of rewriting techniques and their integration in large scale applications. Powerful matching capabilities along with a rich strategy language are among Tom's strong points, making it easy to use and competitive with other rule based languages.

Le me mention that Tom not only adds pattern-matching features to Java (or other target languages), but also proposes a strategic programming library which really brings rewriting to Java. The proposed pattern-matching algorithm is more powerful than the ones usually present in functional languages though, since it supports associative matching with neutral element and recently introduced antipatterns.
Finally, the compilation of Tom programs can generate coq proofs that the semantic of the pattern-matching algorithm is preserved.

It is actively used in both industrial and academic project, including the compiler itself, an implementation of the explicit rewriting calculus and a proof assistant for superdeduction modulo.