What formalisms exist to describe the translation of an abstract syntax tree into another formal language? I'm looking for a declarative formalism to describe the transformation of an abstract syntax tree generated by the parsing of one formal language into second formal language. An example of a transformation that it would have to describe is to transform following,

type Bool : Type {
    value false : Bool;
    value true : Bool;
};


into the following,

$Bool : Type;$

$Bool = (Unit \lor Unit);$

$true : Bool;$

$true = (inj_0 unit);$

$false : Bool;$

$false = (inj_1 unit);$

The only thing I can think of is defining piecewise-defined recursive function with nodes of the abstract syntax tree of the original language as input. Is there not a more concise way of declaring the transformation?

I've already implemented such transformations straightforwardly and compositionally in the programming language Haskell but I'm not doing so well on formalising the tranformation.

Also, to be clear I am not talking about attaching semantic actions t the original grammar (or an attribute grammar) because I assume an abstract syntax tree has already been generated by parsing the first formal language because other analysis and rewriting needs to be done on such a tree.

Note that I have no interest in algorithmic efficiency of such a formalism, I only want to show that a injective function from the original formal language to the second formal language exists.

I know I must have read about this in the formal language literature but I can't think of anything specific. I've probably forgotten something really obvious...

Edit:

What about natural deduction style? How could such translations be represented in natural deduction? I'll have to think about that...
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.