mugen in bib

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}
+}