<p>The thesis presents a type system for a substantial fragment of XML query language Xcerpt. The system is descriptive; the types associated with Xcerpt constructs are sets of data terms and approximate the semantics of the constructs.</p><p>A formalism of Type Definitions, related to XML schema languages, is adopted to specify such sets. The type system is presented as typing rules which provide a basis for type inference and type checking algorithms, used in a prototype implementation. Correctness of the type system wrt. the formal semantics of Xcerpt is proved and exactness of the result types inferred by the system is discussed.</p><p>The usefulness of the approach is illustrated by example runs of the prototype on Xcerpt programs.</p><p>Given a non-recursive Xcerpt program and types of data to be queried, the type system is able to infer a type of results of the program. If additionally a type specification of program results is given, the system is able to prove type correctness of a (possibly recursive) program. Type correctness means that the program produces results of the given type whenever it is applied to data of the given type. Non existence of a correctness proof suggests that the program may be incorrect. Under certain conditions (on the program and on the type specification), the program is actually incorrect whenever the proof attempt fails.</p> / Report code: LiU-TEK-LIC-2006:9