Descriptive Typing Rules for Xcerpt

We present typing rules for the Web query language Xcerpt. The rules provide a descriptive type system: the typing of a program is an ation 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.

• Type: Conference
• Year: 2005
• Where: PPSWR
• Authors: Sacha Berger, Emmanuel Coquery, Wlodzimierz Drabent, Artur Wilk
• Keywords: Internet Technology, PPSWR 2005, Query Language Xcerpt, Soundness Proof, Type System