|
|
|
     |
                                     |
Return to Formal Foundations
Modern database systems provide not only powerful data models but also complex query languages supporting powerful features such as the ability to create new database objects and invocation of arbitrary methods (possibly written in a third-party programming language). In this sense query languages have evolved into powerful programming languages. Surprisingly little work exists utilizing techniques from programming language research to specify and analyse these query languages. This paper provides a formal, high-level operational semantics for a complex-value OQL-like query language that can create fresh database objects, and invoke external methods. We defin ea type system for our query language and prove an important soundness property. We define a simple effect typing discipline to delimit the computational effects within our queries. We prove that this effect system is correct and show how it can be used to detect cases of non-determinism and to define correct query optimizations.
@inproceedings {DBLP:conf/sigmod/Bierman03, author = {Gavin M. Bierman}, booktitle = {SIGMOD Conference}, title = {Formal semantics and analysis of object queries.}, pages = {407-418}, year = {2003}, url = {db/conf/sigmod/sigmod2003.html#Bierman03}, ee = {http://www.acm.org/sigmod/sigmod03/eproceedings/papers/r15p02.pdf}, crossref = {conf/sigmod/2003}, bibsource = {DBLP, http://dblp.uni-trier.de} }  ©2004 Association for Computing Machinery |
