liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Descriptive Types for XML Query Language Xcerpt
Linköping University, Department of Computer and Information Science, TCSLAB - Theoretical Computer Science Laboratory. Linköping University, The Institute of Technology.
2006 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

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.

Place, publisher, year, edition, pages
Institutionen för datavetenskap , 2006. , 108 p.
Series
Linköping Studies in Science and Technology. Thesis, ISSN 0280-7971 ; 1228
Series
Keyword [en]
ype system, XML querying, Xcerpt, type inference, type definitions
National Category
Computer Science
Identifiers
URN: urn:nbn:se:liu:diva-7542ISBN: 91-85497-10-X (print)OAI: oai:DiVA.org:liu-7542DiVA: diva2:22550
Presentation
2006-01-27, Alan Turing, House E, Campus Valla, Campus Valla, Linköpings universitet, Linköping, 13:15 (English)
Opponent
Supervisors
Note
Report code: LiU-TEK-LIC-2006:9Available from: 2006-10-09 Created: 2006-10-09 Last updated: 2009-06-08

Open Access in DiVA

fulltext(822 kB)569 downloads
File information
File name FULLTEXT01.pdfFile size 822 kBChecksum SHA-1
a9a83a4e67a06c4ddfbde5e82886429e9bb5485980fd8d5dd65ec34712a9d9b2d49ed5b5
Type fulltextMimetype application/pdf

Authority records BETA

Wilk, Artur

Search in DiVA

By author/editor
Wilk, Artur
By organisation
TCSLAB - Theoretical Computer Science LaboratoryThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 569 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 292 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf