From f87950915de9398f4a80f5df5f598c49b4255074 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 25 Sep 2021 20:10:30 +0200
Subject: [PATCH] add more bib entries

---
 quox.bib | 80 +++++++++++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 68 insertions(+), 12 deletions(-)

diff --git a/quox.bib b/quox.bib
index 26e3220..ededc1c 100644
--- a/quox.bib
+++ b/quox.bib
@@ -6,20 +6,18 @@
                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},
+  booktitle = {Programming Languages and Systems:
+               30th European Symposium on Programming, ({ESOP} 2021)},
   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},
+% url       = {https://doi.org/10.1007/978-3-030-72019-3\_17},
+  url       = {https://arxiv.org/abs/2010.13163},
   doi       = {10.1007/978-3-030-72019-3\_17}
 }
 
-
 @inproceedings{nuttin,
   author    = {Conor McBride},
   editor    = {Sam Lindley and
@@ -93,10 +91,10 @@
 }
 
 
-% Misc implementation
+% NbE
 
-@article{nbe-abel,
-  title    = {Normalization by Evaluation for Martin-Löf Type Theory with
+@article{nbe-mltt,
+  title    = {Normalization by Evaluation for Martin-L\"of Type Theory with
               One Universe},
   journal  = {Electronic Notes in Theoretical Computer Science},
   volume   = {173},
@@ -109,9 +107,66 @@
   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},
+              Type Theory, Universe}
 }
 
+@inproceedings{nbe-mltt-eq,
+  author    = {Andreas Abel and Thierry Coquand and Peter Dybjer},
+  title     = {Normalization by Evaluation for Martin-L\"of Type Theory with Typed
+               Equality Judgements},
+  booktitle = {22nd {IEEE} Symposium on Logic in Computer Science
+               ({LICS} 2007)},
+  pages     = {3--12},
+  publisher = {{IEEE} Computer Society},
+  year      = {2007},
+% url       = {https://doi.org/10.1109/LICS.2007.33},
+  url       = {https://www.cse.chalmers.se/~abela/lics07.pdf},
+  doi       = {10.1109/LICS.2007.33}
+}
+
+@inproceedings{nbe-cbpv,
+  author    = {Andreas Abel and Christian Sattler},
+  editor    = {Ekaterina Komendantskaya},
+  title     = {Normalization by Evaluation for Call-By-Push-Value and Polarized
+               Lambda Calculus},
+  booktitle = {Proceedings of the 21st International Symposium on Principles and
+               Practice of Programming Languages ({PPDP} 2019)},
+  pages     = {3:1--3:12},
+  publisher = {{ACM}},
+  year      = {2019},
+% url       = {https://doi.org/10.1145/3354166.3354168},
+  url       = {https://www.cse.chalmers.se/~abela/ppdp19.pdf},
+  doi       = {10.1145/3354166.3354168}
+}
+
+@phdthesis{nbe-habil,
+  author = {Andreas Abel},
+  title  = {Normalization by Evaluation: Dependent Types and Impredicativity},
+  year   = {2013},
+  type   = {Habilitation thesis},
+  school = {Institut f\"ur Informatik,
+            Ludwig-Maximilians-Universit\"at M\"unchen},
+  url    = {https://www.cse.chalmers.se/~abela/habil.pdf}
+}
+
+@inproceedings{nbe-delay,
+  author    = {Andreas Abel and James Chapman},
+  editor    = {Paul Levy and Neel Krishnaswami},
+  title     = {Normalization by Evaluation in the Delay Monad:
+               {A} Case Study for Coinduction via Copatterns and Sized Types},
+  booktitle = {Proceedings 5th Workshop on Mathematically Structured
+               Functional Programming (MSFP 2014)},
+  series    = {{EPTCS}},
+  volume    = {153},
+  pages     = {51--67},
+  year      = {2014},
+% url       = {https://doi.org/10.4204/EPTCS.153.4},
+  url       = {https://www.cse.chalmers.se/~abela/eptcs14.pdf},
+  doi       = {10.4204/EPTCS.153.4}
+}
+
+% Misc implementation
+
 @article{expl-sub,
   author    = {Mart{\'{\i}}n Abadi and
                Luca Cardelli and
@@ -125,7 +180,7 @@
   year      = {1991},
 % url       = {https://doi.org/10.1017/S0956796800000186},
   url       = {http://lucacardelli.name/Papers/ExplicitSub.pdf},
-  doi       = {10.1017/S0956796800000186},
+  doi       = {10.1017/S0956796800000186}
 }
 
 @article{modal-mltt,
@@ -142,5 +197,6 @@
   title        = {Implementing a Modal Dependent Type Theory},
   volume       = {3},
   url          = {https://www.jonmsterling.com/pdfs/modal-mltt.pdf},
-  note         = {implementation at \url{https://www.jonmsterling.com/resources/blott.tar.gz}}
+  note         = {implementation at
+                  \url{https://www.jonmsterling.com/resources/blott.tar.gz}}
 }