Cosette
Cosette is an automated SQL solver.
**Note: this repo is now deprecated. Check out our new [QED](https://github.com/qed-solver/) solver!** The project is written primarily in Lean, distributed under the BSD 2-Clause "Simplified" License license, first published in 2016. Key topics include: coq, database, rosette, sql, verification.
Cosette
Note: this repo is now deprecated. Check out our new QED solver!
Cosette is a language, and an automated solver for reasoning SQL equivalences.
- Read Introducing Cosette
- See the Cosette Guide to see how to use Cosette
- Try Cosette online demo
- Check out cosette website for research papers about Cosette
This project is in active development. Shoot us a message (cosette@cs.washington.edu) or create an issue if you find something doesn't work!
Contributors
Showing top 9 contributors by commit count.
Related Repositories
rocq-prover/rocq
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
AbsInt/CompCert
The CompCert formally-verified C compiler
UniMath/UniMath
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
Rocq-zh/SF-zh
《软件基础》中文版
magmide/magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
AeneasVerif/aeneas
A verification toolchain for Rust programs