Cosette is a framework developed using the Coq Proof Assistant and the Rosette solver aided language for solving SQL equivalences in databases. It consists of the following parts:

  1. A symbolic execution engine developed in Rosette to find counter examples of unequal SQL queries
  2. 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.


GitHub Repository of Cosette



If you have any question, want to contribute to the project, or just want to say hi, email us at cosette@cs.washington.edu.


Cosette is developed by the Database Group and the Programming Languages and Software Engineering Group at the University of Washington, the main contributors are:

Shumo Chu

Konstantin Weitz

Chenglong Wang

Alvin Cheung

Dan Suciu