Towards Static Type Checking for XSLT

Abstract

We are concerned about the static type checking problem for XSLT. In the context of XSLT and other XML programming, types are DTDs or schemas, and static type checking is to verify that a program always converts valid source documents into also valid output documents. To achieve static type checking for XSLT, we introduce a subset of XSLT, and an efficient algorithm of backward type inference for that subset. Although our XSLT subset lacks XPath, it includes recursive calls of templates and is powerful enough to capture basic XSLT transformations. Our method is based on Finite Tree Automata (FTA) which provide a rigorous representation of types in XML. Given types of output documents, backward type inference computes types of source documents. The idea of back-ward type inference is borrowed from Milo et al's work, while we reduce the computational complexity in their framework.