some bibs

quox.bib

@@ -165,6 +165,28 @@
   doi       = {10.4204/EPTCS.153.4}
 }
 
+% Misc type stuff
+
+@article{calf,
+  author = {Niu, Yue and Sterling, Jonathan and Grodin, Harrison and
+            Harper, Robert},
+  title = {A Cost-Aware Logical Framework},
+  year = {2022},
+  publisher = {Association for Computing Machinery},
+  volume = {6},
+  number = {POPL},
+  url = {https://doi.org/10.1145/3498670},
+  doi = {10.1145/3498670},
+  journal = {Proc. ACM Program. Lang.},
+  month = {jan},
+  articleno = {9},
+  numpages = {31},
+  keywords = {amortized analysis, phase distinction, algorithm analysis, cost
+    models, proof assistants, mechanized proof, parallel algorithms,
+    noninterference, intensional property, behavioral verification, equational
+    reasoning, recurrence relations, modal type theory}
+}
+
 % Misc implementation
 
 @article{expl-sub,
@@ -200,3 +222,16 @@
   note         = {implementation at
                   \url{https://www.jonmsterling.com/resources/blott.tar.gz}}
 }
+
+@article{cbpv,
+  author    = {Paul Blain Levy},
+  title     = {Call-by-push-value: Decomposing call-by-value and call-by-name},
+  journal   = {High. Order Symb. Comput.},
+  volume    = {19},
+  number    = {4},
+  pages     = {377--414},
+  year      = {2006},
+  % url       = {https://doi.org/10.1007/s10990-006-0480-6},
+  url       = {https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf},
+  doi       = {10.1007/s10990-006-0480-6},
+}