XQTC: A Static Type-Checker for XQuery Using Backward Type Inference
type: Dataset
description: We present a novel technique and a tool for static type-checking of XQuery programs. The tool looks for errors in the program by jointly analyzing the source code of the program, input and output schemas that respectively describe the sets of documents admissible as input and as output of the program. The crux and the novelty of our results reside in the joint use of backward type inference and a two-way logic to represent inferred tree type portions. This allowed us to design and implement a type-checker for XQuery which is more precise and supports a larger XQuery fragment compared to the approaches previously proposed in the literature; in particular compared to the only few actually implemented static type-checkers such as the one in Galax. The whole system uses compilers and a satisfiability solver for deciding containment for two-way regular tree expressions. Our tool takes an XQuery program and two schemas Sin and Sout as input. If the program is found incorrect, then it automatically generates a counter-example valid w.r.t. Sin and such that the program produces an invalid output w.r.t Sout. This counter-example can be used by the programmer to fix the program.
identifier: Report N°: RR-8149
issued: 2026-06-03T20:34:21.327823
language: en
modified: 2026-06-03T20:34:21.327829
contact point: Organization
  fn: CCSD
keyword: infoeu-reposemanticsreport
keyword: infoinfo-wbcomputer-science-csweb
keyword: reports
landing page: https://inria.hal.science/hal-00757867

XQTC: A Static Type-Checker for XQuery Using Backward Type Inference
type: Distribution
format: HTML
issued: 2026-06-03T20:34:21.337020
modified: 2026-06-03T20:34:21.316052
access URL: https://inria.hal.science/hal-00757867

test_moissonnage_selune
type: Agent