### 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.

### License

BSD License

### Topics

- Computer science/Data management systems
- Computer science/Algorithms

### Session Generic_Join

- Generic_Join
- Generic_Join_Correctness
- Examples_Join

### Depends on

- Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic

### Used by

- Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations

## Cite

×

Generic_Join-AFP

    @article{Generic_Join-AFP,
      author  = {Thibault Dardinier},
      title   = {Formalization of Multiway-Join Algorithms},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Generic_Join.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Sep 18, 2019 : Isabelle2019