Abstract - lic thesis Artur Wilk

Descriptive Types for XML Query Language Xcerpt
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. 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. The usefulness
of the approach is illustrated by example runs of the prototype
on Xcerpt programs.

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.

back to main page



Travel reports

Licentiate seminars


Courses Spring 2015


Last modified on December 2005 by Anne Moe