# HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics

arXiv: https://arxiv.org/abs/1607.04822 · HTML: https://mlsanity.com/paper/1607.04822/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Jul 2016.

## Built on by (most cited first, 10 of 10)

- [QUITE: A Query Rewrite System Beyond Rules with LLM Agents](https://mlsanity.com/paper/2506.07675/) (2025)
- [Functional Collection Programming with Semi-Ring Dictionaries](https://mlsanity.com/paper/2103.06376/) (2021)
- [SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification](https://mlsanity.com/paper/2510.26840/) (2025)
- [Can the Rookies Cut the Tough Cookie? Exploring the Use of LLMs for SQL Equivalence Checking](https://mlsanity.com/paper/2412.05561/) (2024)
- [GEqO: ML-Accelerated Semantic Equivalence Detection](https://mlsanity.com/paper/2401.01280/) (2024)
- [SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints](https://mlsanity.com/paper/2603.04334/) (2026)
- [EXPO-SQL: Execution-based Clause-level Policy Optimization for Text-to-SQL](https://mlsanity.com/paper/2606.23693/) (2026)
- [Semantic Parsing Natural Language into Relational Algebra](https://mlsanity.com/paper/2106.13858/) (2021)
- [Fine-Tuning Data Structures for Analytical Query Processing](https://mlsanity.com/paper/2112.13099/) (2021)
- [Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search](https://mlsanity.com/paper/2504.06542/) (2025)

## Abstract (arXiv)

Every database system contains a query optimizer that performs query rewrites. Unfortunately, developing query optimizers remains a highly challenging task. Part of the challenges comes from the intricacies and rich features of query languages, which makes reasoning about rewrite rules difficult. In this paper, we propose a machine-checkable denotational semantics for SQL, the de facto language for relational database, for rigorously validating rewrite rules. Unlike previously proposed semantics that are either non-mechanized or only cover a small amount of SQL language features, our semantics covers all major features of SQL, including bags, correlated subqueries, aggregation, and indexes. Our mechanized semantics, called HoTTSQL, is based on K-Relations and homotopy type theory, where we denote relations as mathematical functions from tuples to univalent types. We have implemented HoTTSQL in Coq, which takes only fewer than 300 lines of code and have proved a wide range of SQL rewrite rules, including those from database research literature (e.g., magic set rewrites) and real-world query optimizers (e.g., subquery elimination). Several of these rewrite rules have never been previously proven correct. In addition, while query equivalence is generally undecidable, we have implemented an automated decision procedure using HoTTSQL for conjunctive queries: a well-studied decidable fragment of SQL that encompasses many real-world queries.