What formalisms exist to describe the translation of an abstract syntax tree into another formal language?
Look at Bob Harper's book. It provides loads of declarative formalisms for specifying programming language semantics and so forth. Chapter 6 describes declaratively how to translate concrete into abstract syntax. You could use the same ideas to translate one language into another.

Following Harper (and many others), you could write rules defined inductively on the structure of your source syntax, as follows:

$\begin{array}{c}
a \leadsto e \qquad b \leadsto f \qquad x=foo(a,b,e,f) \\
\hline
\mathsf{K}~a~b \leadsto \mathsf{S}~e~f~x
\end{array}
$

Here $\mathsf{K}$ is a constructor in your source language and $\mathsf{S}$ is in your target language. $foo$ is some function which may compute other required information (it too could be defined as a set of rules).
The translation function/relation essentially inductively decomposes your source syntax and produces a term in your target. You can also thread through additional information to help with the translation process. For example, your rule could look like:

$\begin{array}{c}
E&#39;\vdash a \leadsto e \qquad E&#39;&#39;\vdash b \leadsto f \qquad x=foo(E,E&#39;,E&#39;&#39;,a,b,e,f) \qquad E&#39; = \cdots
\qquad E&#39;&#39;=\cdots \\
\hline
E\vdash \mathsf{K}~a~b \leadsto \mathsf{S}~e~f~x
\end{array}
$

Here $E$ can store any information that needs to be threaded through.

Note that such specifications differ very little from a standard recursive function defined inductively in the program syntax. But they may be easier to read, and they may actually define a relation, rather than a function, by allowing a little nondeterminism.