@article{Ibaraki,
  author    = {Toshihide Ibaraki and
               Tiko Kameda},
  title     = {On the Optimal Nesting Order for Computing N-Relational Joins},
  journal   = {{ACM} Trans. Database Syst.},
  volume    = {9},
  number    = {3},
  pages     = {482--502},
  year      = {1984},
  url       = {https://doi.org/10.1145/1270.1498},
  doi       = {10.1145/1270.1498},
  timestamp = {Tue, 06 Nov 2018 12:51:47 +0100},
  biburl    = {https://dblp.org/rec/journals/tods/IbarakiK84.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Nonrecursive,
  author    = {Ravi Krishnamurthy and
               Haran Boral and
               Carlo Zaniolo},
  title     = {Optimization of Nonrecursive Queries},
  booktitle = {VLDB'86 Twelfth International Conference on Very Large Data Bases,
               August 25-28, 1986, Kyoto, Japan, Proceedings},
  pages     = {128--137},
  year      = {1986},
  crossref  = {DBLP:conf/vldb/86},
  url       = {http://www.vldb.org/conf/1986/P128.PDF},
  timestamp = {Wed, 29 Mar 2017 16:45:23 +0200},
  biburl    = {https://dblp.org/rec/conf/vldb/KrishnamurthyBZ86.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/vldb/86,
  editor    = {Wesley W. Chu and
               Georges Gardarin and
               Setsuo Ohsuga and
               Yahiko Kambayashi},
  title     = {VLDB'86 Twelfth International Conference on Very Large Data Bases,
               August 25-28, 1986, Kyoto, Japan, Proceedings},
  publisher = {Morgan Kaufmann},
  year      = {1986},
  isbn      = {0-934613-18-4},
  timestamp = {Tue, 10 Aug 2021 14:51:32 +0200},
  biburl    = {https://dblp.org/rec/conf/vldb/86.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@online{QueryCompilers,
  author    = {Guido Moerkotte},
  title     = {Building Query Compilers},
  year      = {2020},
  url       = {https://pi3.informatik.uni-mannheim.de/~moer/querycompiler.pdf},
	urldate   = {2021-12-20},
  timestamp = {Mon, 20 Dec 2021 12:04:47 +0100}
}

@inproceedings{QueryOptimizationOverview,
  author    = {Surajit Chaudhuri},
  editor    = {Alberto O. Mendelzon and
               Jan Paredaens},
  title     = {An Overview of Query Optimization in Relational Systems},
  booktitle = {Proceedings of the Seventeenth {ACM} {SIGACT-SIGMOD-SIGART} Symposium
               on Principles of Database Systems, June 1-3, 1998, Seattle, Washington,
               {USA}},
  pages     = {34--43},
  publisher = {{ACM} Press},
  year      = {1998},
  url       = {https://doi.org/10.1145/275487.275492},
  doi       = {10.1145/275487.275492},
  timestamp = {Thu, 15 Nov 2018 10:37:42 +0100},
  biburl    = {https://dblp.org/rec/conf/pods/Chaudhuri98.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@online{ShortestDiameter,
	title        = {Fast Diameter Estimation},
  author       = {Lukas Stevens and Mohammad Abdulaziz},
	urldate      = {2022-02-04},
	url          = {https://gitlab.lrz.de/ls21/lukas-stevens/fast-diameter-estimation},
}

@online{QueryOptimization,
	title        = {Query Optimization Lecture},
  author       = {Thomas Neumann and Bernhard Radke},
	urldate      = {2021-12-22},
	url          = {https://db.in.tum.de/teaching/ws2021/queryopt/},
}

@online{QueryOptimization-Slide,
	title        = {Query Optimization Lecture - Chapter 3},
  author       = {Thomas Neumann and Bernhard Radke},
	urldate      = {2021-12-22},
	url          = {https://db.in.tum.de/teaching/ws2021/queryopt/slides/chapter3.pdf},
}

@article{Graph_Theory-AFP,
  author  = {Lars Noschinski},
  title   = {Graph Theory},
  journal = {Archive of Formal Proofs},
  month   = apr,
  year    = 2013,
  note    = {\url{https://isa-afp.org/entries/Graph_Theory.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@book{Isabelle-Paper,
  author    = {Lawrence C. Paulson},
  title     = {Isabelle - {A} Generic Theorem Prover},
  series    = {Lecture Notes in Computer Science},
  volume    = {828},
  publisher = {Springer},
  year      = {1994},
  url       = {https://doi.org/10.1007/BFb0030541},
  doi       = {10.1007/BFb0030541},
  isbn      = {3-540-58244-4},
  timestamp = {Tue, 14 May 2019 10:00:35 +0200},
  biburl    = {https://dblp.org/rec/books/sp/Paulson94.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{goo,
  author    = {Leonidas Fegaras},
  editor    = {Gerald Quirchmayr and
               Erich Schweighofer and
               Trevor J. M. Bench{-}Capon},
  title     = {A New Heuristic for Optimizing Large Queries},
  booktitle = {Database and Expert Systems Applications, 9th International Conference,
               {DEXA} '98, Vienna, Austria, August 24-28, 1998, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1460},
  pages     = {726--735},
  publisher = {Springer},
  year      = {1998},
  url       = {https://doi.org/10.1007/BFb0054528},
  doi       = {10.1007/BFb0054528},
  timestamp = {Tue, 14 May 2019 10:00:46 +0200},
  biburl    = {https://dblp.org/rec/conf/dexa/Fegaras98.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@online{progprove,
	title        = {Programming and Proving in Isabelle/HOL},
  author       = {Tobias Nipkow},
  year         = 2021,
	urldate      = {2022-02-07},
	url          = {https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/prog-prove.pdf},
}

@online{locales,
	title        = {Tutorial to Locales and Locale Interpretation},
  author       = {Clemens Ballarin},
	urldate      = {2022-02-07},
	url          = {https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/locales.pdf},
}

@online{functions,
	title        = {Defining Recursive Functions in Isabelle/HOL},
  author       = {Alexander Krauss},
	urldate      = {2022-02-08},
	url          = {https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/functions.pdf},
}