{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:56:00Z","timestamp":1767920160221,"version":"3.49.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100020884","name":"ANID\\\/Doctorado Nacional","doi-asserted-by":"publisher","award":["21221100"],"award-info":[{"award-number":["21221100"]}],"id":[{"id":"10.13039\/501100020884","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Millennium 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":[[2026,1,8]]},"abstract":"<jats:p>Proof assistants based on dependent type theory---such as Agda, Lean, and Rocq---employ  \ndifferent universes to classify types, typically combining a predicative tower for  \ncomputationally relevant types with a possibly impredicative universe for proof-irrelevant  \npropositions. Several other universes with specific logical and computational principles  \nhave been explored in the literature. In general, a universe is characterized by its sort  \n(e.g., Type, Prop, or SProp) and, in the predicative case, by its level. To improve  \nmodularity and better avoid code duplication, sort polymorphism has recently been  \nintroduced and integrated in the Rocq prover.<\/jats:p>\n                  <jats:p>However, we observe that, due to its unbounded formulation, sort polymorphism is currently  \ninsufficiently expressive to abstract over valid definitions with a single polymorphic  \nschema. Indeed, to ensure soundness of a multi-sorted type theory, the interaction between  \ndifferent sorts must be carefully controlled, as exemplified by the forbidden elimination  \nof irrelevant terms to produce relevant ones. As a result, generic functions that  \neliminate values of inductive types from one sort to another cannot be made polymorphic;  \ndually, polymorphic records that encapsulate attributes of different sorts cannot be  \ndefined. This lack of expressiveness also breaks the possibility to infer principal  \ntypes, which is highly desirable for both metatheoretical and practical reasons. To  \naddress these issues, we extend sort polymorphism with bounds that reflect the required  \nelimination constraints on sort variables. We present the metatheory of bounded sort  \npolymorphism, paying particular attention to the consistency of the resulting constraint  \ngraph. We implement bounded sort polymorphism in Rocq and illustrate its benefits  \nthrough concrete examples. Bounded sort polymorphism with elimination constraints is a  \nnatural and general solution that effectively addresses current limitations and fosters  \nthe development of, and practical experimentation with, multi-sorted type theories.<\/jats:p>","DOI":"10.1145\/3776732","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2614-2642","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Bounded Sort Polymorphism with Elimination Constraints"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1719-2654","authenticated-orcid":false,"given":"Johann","family":"Rosain","sequence":"first","affiliation":[{"name":"ENS de Lyon, Lyon, France"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-4140-1351","authenticated-orcid":false,"given":"Tom\u00e1s","family":"D\u00edaz","sequence":"additional","affiliation":[{"name":"University of Chile, Santiago, Chile"},{"name":"University of Nantes, Nantes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-3203","authenticated-orcid":false,"given":"Kenji","family":"Maillard","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6452-8806","authenticated-orcid":false,"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Santiago, Chile"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9881-3696","authenticated-orcid":false,"given":"Th\u00e9o","family":"Winterhalter","sequence":"additional","affiliation":[{"name":"Inria, Gif-sur-Yvette, France"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000130"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_2_1_3_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_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_12"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_8"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_2_1_13_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de Doctorat d\u2019\u00c9tat Universit\u00e9 de Paris VII"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532398"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50940-2_39"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014058"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/645387.651547"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2012.381"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547641"},{"key":"e_1_2_1_21_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."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings 28","author":"de Moura Leonardo","year":"2021","unstructured":"Leonardo de Moura and Sebastian Ullrich. 2021. The lean 4 theorem prover and programming language. In Automated Deduction\u2013CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12\u201315, 2021, Proceedings 28. 625\u2013635."},{"key":"e_1_2_1_24_1","volume-title":"All About Proofs, Proofs for All","author":"Paulin-Mohring Christine","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.). College Publications."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_9"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341712"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704912"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Johann Rosain Tomas D\u00edaz Kenji Maillard Matthieu Sozeau Nicolas Tabareau \u00c9ric Tanter and Th\u00e9o Winterhalter. 2025. Bounded Sort Polymorphism with Elimination Constraints. https:\/\/doi.org\/10.5281\/zenodo.17588484 10.5281\/zenodo.17588484","DOI":"10.5281\/zenodo.17588484"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.46298\/entics.12300"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3706056"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_32"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2022.6"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"The Rocq Development Team. 2025. The Rocq Prover. https:\/\/doi.org\/10.5281\/zenodo.15149629 10.5281\/zenodo.15149629","DOI":"10.5281\/zenodo.15149629"},{"key":"e_1_2_1_35_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. https:\/\/ncatlab.org\/homotopytypetheory\/files\/HTS.pdf"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674647"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776732","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:00:22Z","timestamp":1767898822000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776732"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776732"],"URL":"https:\/\/doi.org\/10.1145\/3776732","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}