diff --git a/quox.bib b/quox.bib
new file mode 100644
index 0000000..580c282
--- /dev/null
+++ b/quox.bib
@@ -0,0 +1,145 @@
+% quantitative stuff
+
+@inproceedings{grtt,
+  author    = {Moon, Benjamin and
+               Eades, III, Harley and
+               Orchard, Dominic},
+  editor    = {Yoshida, Nobuko},
+  title     = {Graded Modal Dependent Type Theory},
+  booktitle = {Programming Languages and Systems - 30th European Symposium on Programming,
+               {ESOP} 2021, Held as Part of the European Joint Conferences on Theory
+               and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg,
+               March 27 - April 1, 2021, Proceedings},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {12648},
+  pages     = {462--490},
+  publisher = {Springer},
+  year      = {2021},
+  url       = {https://doi.org/10.1007/978-3-030-72019-3\_17},
+  doi       = {10.1007/978-3-030-72019-3\_17}
+}
+
+
+@inproceedings{nuttin,
+  author    = {Conor McBride},
+  editor    = {Sam Lindley and
+               Conor McBride and
+               Philip W. Trinder and
+               Donald Sannella},
+  title     = {I Got Plenty o' Nuttin'},
+  booktitle = {A List of Successes That Can Change the World - Essays Dedicated to
+               Philip Wadler on the Occasion of His 60th Birthday},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {9600},
+  pages     = {207--233},
+  publisher = {Springer},
+  year      = {2016},
+% url       = {https://doi.org/10.1007/978-3-319-30936-1\_12},
+  url       = {https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf},
+  doi       = {10.1007/978-3-319-30936-1\_12}
+}
+
+@inproceedings{qtt,
+  author    = {Robert Atkey},
+  editor    = {Anuj Dawar and
+               Erich Gr{\"{a}}del},
+  title     = {Syntax and Semantics of Quantitative Type Theory},
+  booktitle = {Proceedings of the 33rd Annual {ACM/IEEE} Symposium on Logic in Computer
+               Science, {LICS} 2018, Oxford, UK, July 09-12, 2018},
+  pages     = {56--65},
+  publisher = {{ACM}},
+  year      = {2018},
+% url       = {https://doi.org/10.1145/3209108.3209189},
+  url       = {https://bentnib.org/quantitative-type-theory.pdf},
+  doi       = {10.1145/3209108.3209189}
+}
+
+
+% observational stuff
+
+@inproceedings{ott-now,
+  author    = {Thorsten Altenkirch and
+               Conor McBride and
+               Wouter Swierstra},
+  editor    = {Aaron Stump and
+               Hongwei Xi},
+  title     = {Observational equality, now!},
+  booktitle = {Proceedings of the {ACM} Workshop Programming Languages meets Program
+               Verification, {PLPV} 2007, Freiburg, Germany, October 5, 2007},
+  pages     = {57--68},
+  publisher = {{ACM}},
+  year      = {2007},
+% url       = {https://doi.org/10.1145/1292597.1292608},
+  url       = {https://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf},
+  doi       = {10.1145/1292597.1292608}
+}
+
+@inproceedings{xtt,
+  author    = {Jonathan Sterling and
+               Carlo Angiuli and
+               Daniel Gratzer},
+  editor    = {Herman Geuvers},
+  title     = {Cubical Syntax for Reflection-Free Extensional Equality},
+  booktitle = {4th International Conference on Formal Structures for Computation
+               and Deduction, {FSCD} 2019, June 24-30, 2019, Dortmund, Germany},
+  series    = {LIPIcs},
+  volume    = {131},
+  pages     = {31:1--31:25},
+  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
+  year      = {2019},
+% url       = {https://doi.org/10.4230/LIPIcs.FSCD.2019.31},
+  url       = {https://arxiv.org/pdf/1904.08562.pdf},
+  doi       = {10.4230/LIPIcs.FSCD.2019.31}
+}
+
+
+% Misc implementation
+
+@article{nbe-abel,
+  title    = {Normalization by Evaluation for Martin-Löf Type Theory with
+              One Universe},
+  journal  = {Electronic Notes in Theoretical Computer Science},
+  volume   = {173},
+  pages    = {17-39},
+  year     = {2007},
+  note     = {Proceedings of the 23rd Conference on the Mathematical Foundations
+              of Programming Semantics (MFPS XXIII)},
+  issn     = {1571-0661},
+  doi      = {https://doi.org/10.1016/j.entcs.2007.02.025},
+  url      = {https://www.sciencedirect.com/science/article/pii/S1571066107000977},
+  author   = {Andreas Abel and Klaus Aehlig and Peter Dybjer},
+  keywords = {Dependent Types, Domain Semantics, Normalization by Evaluation,
+              Type Theory, Universe},
+}
+
+@article{expl-sub,
+  author    = {Mart{\'{\i}}n Abadi and
+               Luca Cardelli and
+               Pierre{-}Louis Curien and
+               Jean{-}Jacques L{\'{e}}vy},
+  title     = {Explicit Substitutions},
+  journal   = {J. Funct. Program.},
+  volume    = {1},
+  number    = {4},
+  pages     = {375--416},
+  year      = {1991},
+% url       = {https://doi.org/10.1017/S0956796800000186},
+  url       = {http://lucacardelli.name/Papers/ExplicitSub.pdf},
+  doi       = {10.1017/S0956796800000186},
+}
+
+@article{modal-mltt,
+  author       = {Gratzer, Daniel and Sterling, Jonathan and Birkedal, Lars},
+  location     = {New York, NY, USA},
+  publisher    = {ACM},
+  date         = {2019-07},
+  doi          = {10.1145/3341711},
+  issn         = {2475-1421},
+  journaltitle = {Proceedings of the ACM on Programming Languages},
+  keywords     = {Modal types,dependent types,normalization by evaluation,type-checking},
+  number       = {ICFP},
+  pages        = {107:1--107:29},
+  title        = {Implementing a Modal Dependent Type Theory},
+  volume       = {3},
+  url          = {https://www.jonmsterling.com/pdfs/modal-mltt.pdf}
+}