From 1dc0c913e7adab58f3f0779fde5c5c27c182a2c1 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 18 Jan 2023 21:24:45 +0100
Subject: [PATCH] mugen in bib

---
 quox.bib | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/quox.bib b/quox.bib
index 644b4e6..2729e4b 100644
--- a/quox.bib
+++ b/quox.bib
@@ -245,3 +245,34 @@
   url       = {https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf},
   doi       = {10.1007/s10990-006-0480-6},
 }
+
+@article{mugen,
+  author = {Hou (Favonia), Kuen-Bang and Angiuli, Carlo and Mullanix, Reed},
+  title = {An Order-Theoretic Analysis of Universe Polymorphism},
+  year = {2023},
+  issue_date = {January 2023},
+  publisher = {Association for Computing Machinery},
+  address = {New York, NY, USA},
+  volume = {7},
+  number = {POPL},
+  url = {https://doi.org/10.1145/3571250},
+  doi = {10.1145/3571250},
+  abstract = {
+    We present a novel formulation of universe polymorphism in dependent type
+    theory in terms of monads on the category of strict partial orders, and a
+    novel algebraic structure, displacement algebras, on top of which one can
+    implement a generalized form of McBride’s “crude but effective
+    stratification” scheme for lightweight universe polymorphism. We give some
+    examples of exotic but consistent universe hierarchies, and prove that every
+    universe hierarchy in our sense can be embedded in a displacement algebra
+    and hence implemented via our generalization of McBride’s scheme. Many of
+    our technical results are mechanized in Agda, and we have an OCaml library
+    for universe levels based on displacement algebras, for use in proof
+    assistant implementations.
+  },
+  journal = {Proc. ACM Program. Lang.},
+  month = {jan},
+  articleno = {57},
+  numpages = {27},
+  keywords = {universes, type theory, universe polymorphism}
+}