Type Systems for XML

XML is a standard data format that is nowadays used everywhere. A notable feature of XML is its user-definable schemas. Schemas describe structural constraints on XML documents, thus defining “types” of XML. However, in current languages and systems for processing XML, those types are used only for dynamically validating data, not for statically verifying programs.

The goal of this work is to establish methods for the design and implementation of type systems for XML processing. However, this task is not a simple transfer of existing knowledges in programming languages since XML types are based on regular tree expressions and therefore have much richer structure than standard types treated in past researches. More concretely, difficulties arise in finding suitable definitions and algorithms for (1) typing concepts already standard in functional programming, e.g., subtyping and parametric polymorphism, (2) XML-specific structures, e.g., (in addition to regular tree expressions) attribute and shuffle expressions, and (3) language constructs for XML processing, e.g., pattern matching and its extensions. In this talk, I will overview our efforts dealing with these issues, emphasizing the principles consistently used in all of these—”definition by semantics” and “implementation based on finite tree automata.”

This work has been done jointly with Jérôme Vouillon, Benjamin Pierce, Makoto Murata, Tadahiro Suda, Alain Frisch, and Giuseppe Castagna.