Abstract
We present typing rules for the Web query language Xcerpt. The rules provide a descriptive type system: the typing of a program is an approximation of its semantics. The rules can also be seen as an abstract form of a type inference algorithm (presented in previous work), and as a stage in a formal soundness proof of the algorithm. The paper considers a substantial fragment of Xcerpt; the main restriction is that we deal with data terms corresponding to trees (instead of general graphs), and we do not deal with Xcerpt rule chaining. We provide a formal semantics for the fragment of Xcerpt and a soundness theorem for the presented type system. The semantics is a basis for a soundness proof of the typing system, the proof is given in a full version of this paper.

URL:
http://rewerse.net/publications/rewerse-publications.html#REWERSE-TR-2005-01

BibTeX:

@techreport{REWERSE-TR-2005-01,
	author = {Sacha Berger and Emmanuel Coquery and W\lodzimierz Drabent and Artur Wilk},
	title = {Descriptive Typing Rules for Xcerpt and their Soundness},
	institution = {Institute for Informatics, University of Munich},
	year = {2005},
	type = {{research report, REWERSE-TR-2005-01}},
	number = {REWERSE-TR-2005-01},
	url = {http://rewerse.net/publications/rewerse-publications.html#REWERSE-TR-2005-01}
}