{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:05Z","timestamp":1780994705740,"version":"3.54.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Millenium Science Initiative Program","award":["ICN17_002"],"award-info":[{"award-number":["ICN17_002"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>Proof assistants based on dependent type theory, such as Coq, Lean and Agda, use different universes to classify types, typically combining a predicative hierarchy of universes for computationally-relevant types, and an impredicative universe of proof-irrelevant propositions. In general, a universe is characterized by its sort, such as Type or Prop, and its level, in the case of a predicative sort. Recent research has also highlighted the potential of introducing more sorts in the type theory of the proof assistant as a structuring means to address the coexistence of different logical or computational principles, such as univalence, exceptions, or definitional proof irrelevance. This diversity raises concrete and subtle issues from both theoretical and practical perspectives. In particular, in order to avoid duplicating definitions to inhabit all (combinations of) universes, some sort of polymorphism is needed. Universe level polymorphism is well-known and effective to deal with hierarchies, but the handling of polymorphism between sorts is currently ad hoc and limited in all major proof assistants, hampering reuse and extensibility. This work develops sort polymorphism and its metatheory, studying in particular monomorphization, large elimination, and parametricity. We implement sort polymorphism in Coq and present examples from a new sort-polymorphic prelude of basic definitions and automation. Sort polymorphism is a natural solution that effectively addresses the limitations of current approaches and prepares the ground for future multi-sorted type theories.<\/jats:p>","DOI":"10.1145\/3704912","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"2253-2281","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-4463-2773","authenticated-orcid":false,"given":"Josselin","family":"Poiret","sequence":"first","affiliation":[{"name":"Nantes Universit\u00e9, Nantes, France"},{"name":"Inria, Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-0626-3078","authenticated-orcid":false,"given":"Ga\u00ebtan","family":"Gilbert","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-3203","authenticated-orcid":false,"given":"Kenji","family":"Maillard","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-8006-6239","authenticated-orcid":false,"given":"Pierre-Marie","family":"P\u00e9drot","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6452-8806","authenticated-orcid":false,"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Santiago, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636951"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000130"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_3_2_5_1","unstructured":"Bruno Barras. 1999. Auto-validation d\u2019un syst\u00e8me de preuves avec familles inductives. Ph. D. Dissertation. Universit\u00e9 Paris 7."},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_12"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2022.01.017"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_8"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434341"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656379"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_3_2_16_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. (1972). Th\u00e8se de Doctorat d\u2019\u00c9tat Universit\u00e9 de Paris VII."},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532398"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50940-2_39"},{"key":"e_1_3_2_20_1","first-page":"153","volume-title":"International Workshop on Types for Proofs and Programs","author":"Hofmann Martin","year":"1995","unstructured":"Martin Hofmann. 1995. Conservativity of equality reflection over intensional type theory. In International Workshop on Types for Proofs and Programs. Springer, 153\u2013164."},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571250"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2012.381"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2022.28"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547641"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_26_1","unstructured":"P. Letouzey. 2004. Programmation fonctionnelle certifi\u00e9e \u2013 L\u2019extraction de programmes dans l\u2019assistant Coq. Ph. D. Dissertation. Universit\u00e9 Paris-Sud."},{"issue":"3","key":"e_1_3_2_27_1","article-title":"Weak omega-categories from intensional type theory","volume":"6","author":"Lumsdaine Peter LeFanu","year":"2010","unstructured":"Peter LeFanu Lumsdaine. 2010. Weak omega-categories from intensional type theory. Logical Methods in Computer Science 6, 3 (2010).","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_3_2_29_1","unstructured":"Per Martin-L\u00f6f. 1971. An Intuitionistic Theory of Types. Unpublished manuscript."},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_31_1","volume-title":"All about Proofs, Proofs for All","author":"Paulin-Mohring Christine","year":"2015","unstructured":"Christine Paulin-Mohring. 2015. Introduction to the Calculus of Inductive Constructions. In All about Proofs, Proofs for All, Bruno Woltzenlogel Paleo and David Delahaye (Eds.). Studies in Logic (Mathematical logic and foundations), Vol. 55. College Publications. https:\/\/hal.inria.fr\/hal-01094195"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_9"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341712"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_3_2_35_1","volume-title":"The Principles of Mathematics","author":"Russell Bertrand","year":"1903","unstructured":"Bertrand Russell. 1903. The Principles of Mathematics. Cambridge University Press."},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.46298\/ENTICS.12300"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_32"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2022.6"},{"key":"e_1_3_2_42_1","unstructured":"The Coq Development Team. 2022. The Coq proof assistant reference manual. https:\/\/coq.inria.fr\/refman\/ Version 8.15."},{"key":"e_1_3_2_43_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book\/"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_3_2_45_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. https:\/\/ncatlab.org\/homotopytypetheory\/files\/HTS.pdf"},{"key":"e_1_3_2_46_1","unstructured":"Benjamin Werner. 1994. Une Th\u00e9orie des Constructions Inductives. Theses. Universit\u00e9 Paris-Diderot - Paris VII. https:\/\/tel.archives-ouvertes.fr\/tel-00196524"},{"key":"e_1_3_2_47_1","unstructured":"Th\u00e9o Winterhalter. 2024. Dependent Ghosts Have a Reflection for Free. (Feb. 2024). https:\/\/hal.science\/hal-04163836 to be published at ICFP\u201924."},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294095"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704912","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704912","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:30Z","timestamp":1770200310000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704912"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704912"],"URL":"https:\/\/doi.org\/10.1145\/3704912","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}