XML documents are often generated by some application in order to be processed by a another program. For a correct exchange of information it has to be guaranteed that for correct inputs only correct outputs are produced. The shape of correct documents, i.e., their type, is usually specified by means of schema languages.
This thesis is concerned with methods for statically guaranteeing that transformations are correct with respect to pre-defined types. Therefore, we consider the XML transformation language TL abstracting the key features of common XML transformation languages.
We show that each TL program can be decomposed into at most three stay macro tree transducers. By means of classical results for stay macro tree transducers, this decomposition allows to formulate a type checking algorithm for TL. This method, however, has even for small programs an exorbitant run-time.
Therefore, we develop an alternative approach, which allows at least for a large class of transformations that they can be type checked in polynomial time. The developed algorithms have been implemented and tested for practical examples.