- A symbolic execution engine developed in Rosette to find counter examples of unequal SQL queries
- HoTTSQL, a SQL like language and its machine checkable denotational semantics in Coq.
- HoTTSQL covers all major SQL features, including selection-projection-join, aggregation, correlated subqueries, and indexes. We provide a machine checkable denotational semantics of HoTTSQL using Homotopy Type Theory for proving rewriting rules.
- A library that consists of building blocks of proofs and automatic decision procedures (e.g., decision procedure for conjunctive queries).
- Machine checkable proofs for existing rewrite rules from database literature as well as real-world optimizers, ranging from basic ones such as selection push down to complex ones such as magic sets rewrites.
- Cosette: An Automated Prover For SQL CIDR 2017 (to appear)
- Post on the Homotopy Type Theory Blog
- HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics (preprint)
If you have any question, want to contribute to the project, or just want to say hi, email us at firstname.lastname@example.org.
Cosette is developed by the Database Group and the Programming Languages and Software Engineering Group at the University of Washington, the main contributors are: