references.bib

% SPDX-License-Identifier: MPL-2.0
%
% References for QuandleDB/KRL: knot-theory database with HoTT-based equality
%

@book{hottbook2013,
  author    = {{The Univalent Foundations Program}},
  title     = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {Institute for Advanced Study},
  year      = {2013},
  note      = {Defines HoTT and the univalence axiom. QuandleDB's equality
               semantics are grounded in HoTT's identity types, where
               equivalence of knot invariants constitutes a path in the
               type-theoretic sense.}
}

@inproceedings{willsey2021,
  author    = {Max Willsey and Chandrakana Nandi and Yisu Remy Wang
               and Oliver Flatt and Zachary Tatlock and Pavel Panchekha},
  title     = {egg: Fast and Extensible Equality Saturation},
  journal   = {Proceedings of the ACM on Programming Languages (POPL)},
  volume    = {5},
  pages     = {1--29},
  year      = {2021},
  note      = {Introduces e-graph based equality saturation. QuandleDB uses
               equality saturation for query optimisation, identifying
               equivalent knot representations via Reidemeister moves.}
}

@inproceedings{chu2017,
  author    = {Shumo Chu and Konstantin Weitz and Alvin Cheung
               and Dan Suciu},
  title     = {{HoTTSQL}: Proving Query Rewrites with Univalent {SQL}
               Semantics},
  booktitle = {Proceedings of the ACM SIGPLAN Conference on Programming
               Language Design and Implementation (PLDI)},
  pages     = {510--524},
  year      = {2017},
  publisher = {ACM},
  note      = {Applies HoTT to prove SQL query equivalences. QuandleDB extends
               this approach from relational algebra to knot-theoretic query
               algebra, where equivalence is defined by knot invariants.}
}

@inproceedings{spivak2012,
  author    = {David I. Spivak},
  title     = {Functorial Data Migration},
  journal   = {Information and Computation},
  volume    = {217},
  pages     = {31--51},
  year      = {2012},
  note      = {Defines CQL (Categorical Query Language) using functorial
               semantics. QuandleDB's schema migrations are expressed as
               functors between knot-theoretic categories.}
}

@misc{livingston2023,
  author    = {Charles Livingston and Allison H. Moore},
  title     = {{KnotInfo}: Table of Knot Invariants},
  howpublished = {\url{https://www.indiana.edu/~knotinfo/}},
  year      = {2023},
  note      = {Comprehensive database of knot invariants. QuandleDB's initial
               data set and invariant validation are benchmarked against
               KnotInfo's tables.}
}

@article{joyce1982,
  author    = {David Joyce},
  title     = {A Classifying Invariant of Knots, the Knot Quandle},
  journal   = {Journal of Pure and Applied Algebra},
  volume    = {23},
  number    = {1},
  pages     = {37--65},
  year      = {1982},
  note      = {Introduces the knot quandle as a complete knot invariant.
               QuandleDB is named after and built upon the quandle algebraic
               structure as its fundamental data organisation principle.}
}

@article{reidemeister1927,
  author    = {Kurt Reidemeister},
  title     = {Elementare Begr\"{u}ndung der Knotentheorie},
  journal   = {Abhandlungen aus dem Mathematischen Seminar der Universit\"{a}t
               Hamburg},
  volume    = {5},
  pages     = {24--32},
  year      = {1927},
  note      = {Establishes the three Reidemeister moves as generators of knot
               equivalence. KRL query normalisation applies Reidemeister moves
               to canonicalise knot diagram representations in the database.}
}

@article{green2007,
  author    = {Todd J. Green and Grigoris Karvounarakis and Val Tannen},
  title     = {Provenance Semirings},
  booktitle = {Proceedings of the ACM SIGMOD-SIGACT-SIGART Symposium on
               Principles of Database Systems (PODS)},
  pages     = {31--40},
  year      = {2007},
  publisher = {ACM},
  note      = {Unifies provenance tracking via semiring annotations. QuandleDB
               tracks the provenance of knot equivalence proofs using
               semiring-annotated derivation trees.}
}

@article{matveev2003,
  author    = {Sergei V. Matveev},
  title     = {Distributive Groupoids in Knot Theory},
  journal   = {Sbornik: Mathematics},
  volume    = {119},
  number    = {1},
  pages     = {78--88},
  year      = {1982},
  note      = {Independent co-discovery of quandle-like structures (called
               distributive groupoids). Provides alternative axiomatisation
               used in QuandleDB's algebraic normalisation engine.}
}

@article{nelson2003,
  author    = {Sam Nelson},
  title     = {A Polynomial Invariant of Finite Quandles},
  journal   = {Journal of Algebra and Its Applications},
  volume    = {2},
  number    = {3},
  pages     = {263--286},
  year      = {2003},
  note      = {Defines polynomial invariants for finite quandles. QuandleDB
               uses these polynomials as hash keys for efficient lookup of
               equivalent knot representations.}
}

@inproceedings{willsey2023,
  author    = {Max Willsey and Philip Zucker and Remy Wang and Oliver Flatt
               and Zachary Tatlock},
  title     = {egglog: Combining E-Graphs and Datalog},
  year      = {2023},
  note      = {Merges e-graph equality saturation with Datalog-style queries.
               QuandleDB's KRL draws on egglog's design to combine
               knot-equivalence reasoning with declarative queries.}
}