{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:17:02Z","timestamp":1767928622593,"version":"3.49.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-21-0009"],"award-info":[{"award-number":["FA9550-21-0009"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>\n            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,\n            <jats:italic>displacement algebras,<\/jats:italic>\n            on top of which one can implement a generalized form of McBride\u2019s \u201ccrude but effective stratification\u201d 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\u2019s 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.\n          <\/jats:p>","DOI":"10.1145\/3571250","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1659-1685","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["An Order-Theoretic Analysis of Universe Polymorphism"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2310-3673","authenticated-orcid":false,"given":"Kuen-Bang","family":"Hou (Favonia)","sequence":"first","affiliation":[{"name":"University of Minnesota, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9590-3303","authenticated-orcid":false,"given":"Carlo","family":"Angiuli","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7970-4961","authenticated-orcid":false,"given":"Reed","family":"Mullanix","sequence":"additional","affiliation":[{"name":"University of Minnesota, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.274.1"},{"key":"e_1_2_1_2_1","unstructured":"Danil Annenkov Paolo Capriotti and Nicolai Kraus. 2017. Two-Level Type Theory and Applications. arxiv:cs.LO\/1705.03307 http:\/\/arxiv.org\/abs\/1705.03307 Preprint. \t\t\t\t  Danil Annenkov Paolo Capriotti and Nicolai Kraus. 2017. Two-Level Type Theory and Applications. arxiv:cs.LO\/1705.03307 http:\/\/arxiv.org\/abs\/1705.03307 Preprint."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2022.01.017"},{"key":"e_1_2_1_5_1","unstructured":"Marc Bezem Thierry Coquand Peter Dybjer and Mart\u00edn Escard\u00f3. 2022. Type Theories with Universe Level Judgments. https:\/\/types22.inria.fr\/files\/2022\/06\/TYPES_2022_paper_56.pdf \t\t\t\t  Marc Bezem Thierry Coquand Peter Dybjer and Mart\u00edn Escard\u00f3. 2022. Type Theories with Universe Level Judgments. https:\/\/types22.inria.fr\/files\/2022\/06\/TYPES_2022_paper_56.pdf"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_4"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS","author":"Coquand Thierry","year":"1986","unstructured":"Thierry Coquand . 1986 . An Analysis of Girard\u2019s Paradox . In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986). IEEE Computer Society Press, 227\u2013236. Thierry Coquand. 1986. An Analysis of Girard\u2019s Paradox. In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986). IEEE Computer Society Press, 227\u2013236."},{"key":"e_1_2_1_9_1","unstructured":"Thierry Coquand. 2013. Presheaf model of type theory. (2013). http:\/\/www.cse.chalmers.se\/~coquand\/presheaf.pdf Unpublished note. \t\t\t\t  Thierry Coquand. 2013. Presheaf model of type theory. (2013). http:\/\/www.cse.chalmers.se\/~coquand\/presheaf.pdf Unpublished note."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.01.015"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_9"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218216518410018"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90108-T"},{"key":"e_1_2_1_18_1","unstructured":"G\u00e9rard Huet. 1987. Extending the calculus of constructions with Type:Type. (1987). http:\/\/pauillac.inria.fr\/~huet\/PUBLIC\/typtyp.pdf Unpublished note. \t\t\t\t  G\u00e9rard Huet. 1987. Extending the calculus of constructions with Type:Type. (1987). http:\/\/pauillac.inria.fr\/~huet\/PUBLIC\/typtyp.pdf Unpublished note."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2022.28"},{"key":"e_1_2_1_20_1","unstructured":"Per Martin-L\u00f6f. 1971. An intuitionistic theory of types. (1971). Unpublished preprint. \t\t\t\t  Per Martin-L\u00f6f. 1971. An intuitionistic theory of types. (1971). Unpublished preprint."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_2_1_22_1","unstructured":"Conor McBride. 2002. Crude but Effective Stratification. https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/Crude.pdf Slides. \t\t\t\t  Conor McBride. 2002. Crude but Effective Stratification. https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/Crude.pdf Slides."},{"key":"e_1_2_1_23_1","unstructured":"Conor McBride. 2011. Crude but Effective Stratification. https:\/\/mazzo.li\/epilogue\/index.html \t\t\t\t  Conor McBride. 2011. Crude but Effective Stratification. https:\/\/mazzo.li\/epilogue\/index.html"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.001.0001"},{"key":"e_1_2_1_26_1","unstructured":"RedPRL Development Team. 2022. mugen. https:\/\/github.com\/RedPRL\/mugen \t\t\t\t  RedPRL Development Team. 2022. mugen. https:\/\/github.com\/RedPRL\/mugen"},{"key":"e_1_2_1_27_1","unstructured":"RedPRL Development Team. 2022. 133 177 96algaett. https:\/\/github.com\/RedPRL\/algaett \t\t\t\t  RedPRL Development Team. 2022. 133 177 96algaett. https:\/\/github.com\/RedPRL\/algaett"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050140"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_32"},{"key":"e_1_2_1_30_1","unstructured":"Yuta Takahashi. 2022. Higher-Order Universe Operators in Martin-L\u00f6f Type Theory with one Mahlo Universe. https:\/\/types22.inria.fr\/files\/2022\/06\/TYPES_2022_paper_63.pdf \t\t\t\t  Yuta Takahashi. 2022. Higher-Order Universe Operators in Martin-L\u00f6f Type Theory with one Mahlo Universe. https:\/\/types22.inria.fr\/files\/2022\/06\/TYPES_2022_paper_63.pdf"},{"key":"e_1_2_1_31_1","unstructured":"The 1Lab Development Team. 2022. The 1Lab. https:\/\/1lab.dev \t\t\t\t  The 1Lab Development Team. 2022. The 1Lab. https:\/\/1lab.dev"},{"key":"e_1_2_1_32_1","unstructured":"The Agda Development Team. 2022. The Agda Programming Language. https:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php \t\t\t\t  The Agda Development Team. 2022. The Agda Programming Language. https:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php"},{"key":"e_1_2_1_33_1","unstructured":"The Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/www.coq.inria.fr \t\t\t\t  The Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/www.coq.inria.fr"},{"key":"e_1_2_1_34_1","unstructured":"The HELM Team. 2016. Matita. http:\/\/matita.cs.unibo.it\/index.shtml \t\t\t\t  The HELM Team. 2016. Matita. http:\/\/matita.cs.unibo.it\/index.shtml"},{"key":"e_1_2_1_35_1","unstructured":"The LEGO Team. 1999. The LEGO Proof Assistant. https:\/\/www.dcs.ed.ac.uk\/home\/lego\/ \t\t\t\t  The LEGO Team. 1999. The LEGO Proof Assistant. https:\/\/www.dcs.ed.ac.uk\/home\/lego\/"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571250","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571250","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571250"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":34,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571250"],"URL":"https:\/\/doi.org\/10.1145\/3571250","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}