| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Formalization of Multiway-Join Algorithms
| Title: | Formalization of Multiway-Join Algorithms |
| Author: | Thibault Dardinier |
| Submission date: | 2019-09-16 |
| Abstract: | Worst-case optimal multiway-join algorithms are recent seminal achievement of the database community. These algorithms compute the natural join of multiple relational databases and improve in the worst case over traditional query plan optimizations of nested binary joins. In 2014, Ngo, Ré, and Rudra gave a unified presentation of different multi-way join algorithms. We formalized and proved correct their "Generic Join" algorithm and extended it to support negative joins. |
| BibTeX: |
@article{Generic_Join-AFP,
author = {Thibault Dardinier},
title = {Formalization of Multiway-Join Algorithms},
journal = {Archive of Formal Proofs},
month = sep,
year = 2019,
note = {\url{http://isa-afp.org/entries/Generic_Join.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | MFOTL_Monitor |
| Used by: | MFODL_Monitor_Optimized |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |