Projects per year
Abstract / Description of output
Language-integrated query is a powerful programming construct allowing database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query techniques rely on classical results about the nested relational calculus, stating that its queries can be algorithmically translated to SQL, as long as their result type is a flat relation. Cooper and others advocated higher-order nested relational calculi as a basis for language-integrated queries in functional languages such as Links and F#. However, the translation of higher-order relational queries to SQL relies on a rewrite system for which no strong normalization proof has been published: a previous proof attempt does not deal correctly with rewrite rules that duplicate subterms. This paper fills the gap in the literature, explaining the difficulty with a previous proof attempt, and showing how to extend the ⊤⊤-lifting approach of Lindley and Stark to accommodate duplicating rewrites. We also show how to extend the proof to a recently-introduced calculus for heterogeneous queries mixing set and multiset semantics.
Original language | English |
---|---|
Article number | 23 |
Pages (from-to) | 23:1-23:41 |
Number of pages | 41 |
Journal | Logical Methods in Computer Science |
Volume | 18 |
Issue number | 3 |
DOIs | |
Publication status | Published - 17 Aug 2022 |
Keywords / Materials (for Non-textual outputs)
- Strong normalization
- ⊤⊤-lifting
- Nested relational calculus
- Language-integrated query
Fingerprint
Dive into the research topics of 'Strongly-Normalizing Higher-Order Relational Queries'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Skye-A programming language bridging theory and practice for scientific data curation
1/09/16 → 28/02/23
Project: Research