{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:15:42Z","timestamp":1784211342641,"version":"3.55.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"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>\n                    Proof assistants based on dependent type theory\u2014such as\n                    <jats:sc>Agda<\/jats:sc>\n                    ,\n                    <jats:sc>Lean<\/jats:sc>\n                    , and\n                    <jats:sc>Rocq<\/jats:sc>\n                    \u2014employ different universes to classify types, typically combining a predicative tower for computationally relevant types with a possibly impredicative universe for proof-irrelevant propositions. Several other universes with specific logical and computational principles have been explored in the literature. In general, a universe is characterized by its sort (e.g., Type, Prop, or SProp) and, in the predicative case, by its level. To improve modularity and better avoid code duplication, sort polymorphism has recently been introduced and integrated in the\n                    <jats:sc>Rocq<\/jats:sc>\n                    prover.\n                  <\/jats:p>\n                  <jats:p>\n                    However, we observe that, due to its unbounded formulation, sort polymorphism is currently insufficiently expressive to abstract over valid definitions with a single polymorphic schema. Indeed, to ensure soundness of a multi-sorted type theory, the interaction between different sorts must be carefully controlled, as exemplified by the forbidden elimination of irrelevant terms to produce relevant ones. As a result, generic functions that eliminate values of inductive types from one sort to another cannot be made polymorphic; dually, polymorphic records that encapsulate attributes of different sorts cannot be defined. This lack of expressiveness also breaks the possibility to infer principal types, which is highly desirable for both metatheoretical and practical reasons. To address these issues, we extend sort polymorphism with bounds that reflect the required elimination constraints on sort variables. We present the metatheory of bounded sort polymorphism, paying particular attention to the consistency of the resulting constraint graph. We implement bounded sort polymorphism in\n                    <jats:sc>Rocq<\/jats:sc>\n                    and illustrate its benefits through concrete examples. Bounded sort polymorphism with elimination constraints is a natural and general solution that effectively addresses current limitations and fosters the development of, and practical experimentation with, multi-sorted type theories.\n                  <\/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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"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\/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"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000130"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_3_2_4_1","unstructured":"Bruno Barras. 1999. Auto-validation d\u1fbfun syst\u00e8me de preuves avec familles inductives. Ph.D. Dissertation. Universit\u00e9 Paris 7."},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_12"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","unstructured":"Ana Bove Peter Dybjer and Ulf Norell. 2009. A Brief Overview of Agda - A Functional Language with Dependent Types. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009). Springer-Verlag Munich Germany 73\u201378. https:\/\/doi.org\/10.1007\/978-3-642-03359-9_6 10.1007\/978-3-642-03359-9_6","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_7_1","first-page":"115","volume-title":"Types for Proofs and Programs","author":"Brady Edwin","year":"2003","unstructured":"Edwin Brady, Conor McBride, and James McKinna. 2003. Inductive Families Need Not Store Their Indices. In Types for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 115\u2013129."},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_3_2_14_1","volume-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u1fbfarithm\u00e9tique d\u1fbfordre sup\u00e9rieur (1972)","author":"Girard Jean-Yves","year":"1972","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u1fbfarithm\u00e9tique d\u1fbfordre sup\u00e9rieur (1972). Th\u00e8se de Doctorat d\u1fbf\u00c9tat, Universit\u00e9 de Paris VII."},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","unstructured":"Daniel Gratzer. 2022. Normalization for Multimodal Type Theory. In LICS \u1fbf22: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science Haifa Israel August 2 - 5 2022 Christel Baier and Dana Fisman (Eds.). ACM 2:1\u20132:13. https:\/\/doi.org\/10.1145\/3531130.3532398 10.1145\/3531130.3532398","DOI":"10.1145\/3531130.3532398"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50940-2_39"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671442"},{"key":"e_1_3_2_19_1","doi-asserted-by":"crossref","unstructured":"Stefan Kaes. 1988. Parametric Overloading in Polymorphic Programming Languages. In Proceedings of the 2nd European Symposium on Programming (ESOP \u201988). 131\u2013144.","DOI":"10.1007\/3-540-19027-9_9"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","unstructured":"Chantal Keller and Marc Lasson. 2012. Parametricity in an Impredicative Sort. In Computer Science Logic (CSL\u1fbf12) - 26th International Workshop\/21st Annual Conference of the EACSL CSL 2012 September 3-6 2012 Fontainebleau France (LIPIcs Vol. 16) Patrick C\u00e9gielski and Arnaud Durand (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 381\u2013395. https:\/\/doi.org\/10.4230\/LIPICS.CSL.2012.381 10.4230\/LIPICS.CSL.2012.381","DOI":"10.4230\/LIPICS.CSL.2012.381"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547641"},{"key":"e_1_3_2_22_1","volume-title":"Programmation fonctionnelle certifi\u00e9e - L\u1fbfextraction de programmes dans l\u1fbfassistant Coq","author":"Letouzey P.","year":"2004","unstructured":"P. Letouzey. 2004. Programmation fonctionnelle certifi\u00e9e - L\u1fbfextraction de programmes dans l\u1fbfassistant Coq. Ph. D. Dissertation. Universit\u00e9 Paris-Sud."},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_25_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.). College Publications."},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_9"},{"key":"e_1_3_2_27_1","doi-asserted-by":"crossref","unstructured":"Pierre-Marie P\u00e9drot Nicolas Tabareau Hans Jacob Fehrmann and \u00c9ric Tanter. 2019. A Reasonably Exceptional Type Theory. Proceedings of the ACM on Programming Languages 3 ICFP Article 108 (July 2019) 29 pages. https:\/\/doi.org\/10.11453341712 10.11453341712","DOI":"10.1145\/3341712"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704912"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Johann Rosain Tomas Diaz 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_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.46298\/ENTICS.12300"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3706056"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_32"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2022.6"},{"key":"e_1_3_2_35_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_3_2_36_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_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_2_38_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,7,16]],"date-time":"2026-07-16T13:39:30Z","timestamp":1784209170000},"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"}}]}}