XML Type Checking with Macro Tree Transducers Sebastian Maneth, Alexandru Berlea, and Thomas Perst   View Paper (PDF)   Return to Research Session 8: Information Processing on the Web Abstract MSO logic on unranked trees has been identified as a convenient theoretical framework for reasoning about expressiveness and implementations of practical XML query languages. As a corresponding theoretical foundation of XML transformation languages, the .transformation language. TL is proposed. This language is based on the .document transformation language. DTL of Maneth and Neven which incorporates full MSO pattern matching, arbitrary navigation in the input tree using also MSO patterns, and named procedures. The new language generalizes DTL by additionally allowing procedures to accumulate intermediate results in parameters. It is proved that TL . and thus in particular DTL . despite their expressiveness still allow for effective inverse type inference. This result is obtained by means of a translation of TL programs into compositions of top-down finite state tree transductions with parameters, also called (stay) macro tree transducers. ©2006 Association for Computing Machinery