{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:46:33Z","timestamp":1770273993733,"version":"3.49.0"},"reference-count":83,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","award":["PTDC\/CCI-COM\/6453\/2020,UIDB\/00408\/2020,UIDP\/00408\/2020"],"award-info":[{"award-number":["PTDC\/CCI-COM\/6453\/2020,UIDB\/00408\/2020,UIDP\/00408\/2020"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this setting, we describe a notion of parametricity for type constructors and then exploit it to define\n            <jats:italic toggle=\"yes\">parametric subtyping<\/jats:italic>\n            , a conceptually simple, decidable, and expressive fragment of structural subtyping that strictly generalizes\n            <jats:italic toggle=\"yes\">rigid subtyping<\/jats:italic>\n            . We present and prove correct an effective saturation-based decision procedure for parametric subtyping, demonstrating its applicability using a variety of examples. We also provide an implementation of this decision procedure as an artifact.\n          <\/jats:p>","DOI":"10.1145\/3632932","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2700-2730","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Parametric Subtyping for Structural Parametric Polymorphism"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1649-9953","authenticated-orcid":false,"given":"Henry","family":"DeYoung","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1547-0692","authenticated-orcid":false,"given":"Andreia","family":"Mordido","sequence":"additional","affiliation":[{"name":"Universidade de Lisboa, Lisbon, Portugal"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8279-5817","authenticated-orcid":false,"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2459-1258","authenticated-orcid":false,"given":"Ankush","family":"Das","sequence":"additional","affiliation":[{"name":"Amazon, Santa Clara, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Mart\u00edn Abadi Luca Cardelli and Ramesh Viswanathan. 1996. An Interpretation of Objects and Object Types. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 396\u2013409. https:\/\/doi.org\/10.1145\/237721.237809 10.1145\/237721.237809","DOI":"10.1145\/237721.237809"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000022"},{"key":"e_1_3_1_4_1","volume-title":"Semantics of Types for Mutable State","author":"Ahmed Amal J.","year":"2004","unstructured":"Amal J. Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. Princeton University. http:\/\/www.ccs.neu.edu\/home\/amal\/ahmedsthesis.pdf AAI3136691."},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2022.104948"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/9783-030-45237-7_3"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"David Baelde Amina Doumane Denis Kuperberg and Alexis Saurin. 2022. Bouncing Threads for Circular and Non-Wellfounded Proofs. In Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science. Article 63 13 pages. https:\/\/doi.org\/10.1145\/3531130.3533375 10.1145\/3531130.3533375","DOI":"10.1145\/3531130.3533375"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/174130.174141"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80025-X"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054285"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1998-33401"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Luca Cardelli. 1984. A Semantics of Multiple Inheritance. In Semantics of Data Types. 51\u201367. https:\/\/doi.org\/10.1007\/3-540-13346-1_2 10.1007\/3-540-13346-1_2","DOI":"10.1007\/3-540-13346-1_2"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17184-3_38"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Luca Cardelli. 1988. Structural Subtyping and the Notion of Power Type. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 70\u201379. https:\/\/doi.org\/10.1145\/73560.73566 10.1145\/73560.73566","DOI":"10.1145\/73560.73566"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"Giuseppe Castagna and Alain Frisch. 2005. A Gentle Introduction to Semantic Subtyping. In Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 198\u2013208. https:\/\/doi.org\/10.1145\/1069774.1069793 10.1145\/1069774.1069793","DOI":"10.1145\/1069774.1069793"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","unstructured":"Giuseppe Castagna and Benjamin C. Pierce. 1994. Decidable Bounded Quantification. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 151\u2013162. https:\/\/doi.org\/10.1145\/174675.177844 10.1145\/174675.177844","DOI":"10.1145\/174675.177844"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000803"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Nils Anders Danielsson and Thorsten Altenkirch. 2010. Subtyping Declaratively. In Mathematics of Program Construction. 100\u2013118. https:\/\/doi.org\/10.1007\/978-3-642-13321-3_8 10.1007\/978-3-642-13321-3_8","DOI":"10.1007\/978-3-642-13321-3_8"},{"key":"e_1_3_1_26_1","unstructured":"Ankush Das Henry DeYoung Andreia Mordido and Frank Pfenning. 2021. Subtyping on Nested Polymorphic Session Types. arXiv:2103.15193 [cs.PL]"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3539656"},{"key":"e_1_3_1_28_1","volume-title":"Practical Refinement-Type Checking","author":"Davies Rowan","year":"2005","unstructured":"Rowan Davies. 2005. Practical Refinement-Type Checking. Ph. D. Dissertation. Carnegie Mellon University. http:\/\/reportsarchive.adm.cs.cmu.edu\/anon\/2005\/CMU-CS-05-110.pdf"},{"key":"e_1_3_1_29_1","doi-asserted-by":"crossref","unstructured":"Henry DeYoung Andreia Mordido Frank Pfenning and Ankush Das. 2023a. Parametric Subtyping for Structural Parametric Polymorphism. arXiv:2307.13661 [cs.PL]","DOI":"10.1145\/3632932"},{"key":"e_1_3_1_30_1","doi-asserted-by":"crossref","unstructured":"Henry DeYoung Andreia Mordido Frank Pfenning and Ankush Das. 2023b. Parametric Subtyping for Structural Parametric Polymorphism (Artifact). https:\/\/zenodo.org\/records\/8423335","DOI":"10.1145\/3632932"},{"key":"e_1_3_1_31_1","unstructured":"Henry DeYoung Andreia Mordido Frank Pfenning and Ankush Das. 2023c. Standard ML Implementation of Parametric Subtyping Decision Procedure. https:\/\/bitbucket.org\/structural-types\/polyte"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Stephen Dolan and Alan Mycroft. 2017. Polymorphism Subtyping and Type Inference in MLsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 60\u201372. https:\/\/doi.org\/10.1145\/3009837.3009882 10.1145\/3009837.3009882","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Derek Dreyer Amal Ahmed and Lars Birkedal. 2009. Logical Step-Indexed Logical Relations. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science. 71\u201380. https:\/\/doi.org\/10.1109\/LICS.2009.34 10.1109\/LICS.2009.34","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"Jana Dunfield and Frank Pfenning. 2004. Tridirectional Typechecking. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 281\u2013292. https:\/\/doi.org\/10.1145\/964001.964025 10.1145\/964001.964025","DOI":"10.1145\/964001.964025"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Tim Freeman and Frank Pfenning. 1991. Refinement Types for ML. In Proceedings of the ACM SIGPLAN 1991 Conference on Language Design and Implementation. 268\u2013277. https:\/\/doi.org\/10.1145\/113445.113468 10.1145\/113445.113468","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90074-8"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","unstructured":"Alain Frisch Giuseppe Castagna and V\u00e9ronique Benzaken. 2002. Semantic Subtyping. In Proceedings of the 17th IEEE Symposium on Logic in Computer Science. 137\u2013146. https:\/\/doi.org\/10.1109\/LICS.2002.1029823 10.1109\/LICS.2002.1029823","DOI":"10.1109\/LICS.2002.1029823"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99253-8_18"},{"key":"e_1_3_1_40_1","volume-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur","author":"Girard Jean-Yves","year":"1972","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph. D. Dissertation. \u00c9diteur inconnu."},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594308"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321254"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009871"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1101"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003713"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_3_1_47_1","volume-title":"Datatypes and Subtyping","author":"Hosoya Haruo","year":"1998","unstructured":"Haruo Hosoya, Benjamin C. Pierce, and David N. Turner. 1998. Datatypes and Subtyping. (1998). Unpublished manuscript."},{"key":"e_1_3_1_48_1","volume-title":"Resolution d\u2019Equations dans des Langages d\u2019Order 1, 2.","author":"Huet G\u00e9rard","year":"1976","unstructured":"G\u00e9rard Huet. 1976. Resolution d\u2019Equations dans des Langages d\u2019Order 1, 2., \u03c9. Ph. D. Dissertation. Universite de Paris VII."},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002643"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","unstructured":"Joxan Jaffar and J.-L. Lassez. 1987. Constraint Logic Programming. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 111\u2013119. https:\/\/doi.org\/10.1145\/41625.41635 10.1145\/41625.41635","DOI":"10.1145\/41625.41635"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2020.07.004"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-17(4:23)2021"},{"key":"e_1_3_1_53_1","unstructured":"Dinesh Katiyar and Sriram Sankar. 1992. Completely Bounded Quantification Is Decidable. In ACM SIGPLAN Workshop on ML and its Applications."},{"key":"e_1_3_1_54_1","unstructured":"Andrew J. Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with Variance. In FOOL-WOOD 2007. http:\/\/www.cis.upenn.edu\/bcpierce\/papers\/variance.pdf"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","unstructured":"A. J. Korenjak and J. E. Hopcroft. 1966. Simple Deterministic Languages. In 7th Annual Symposium on Switching and Automata Theory. 36\u201346. https:\/\/doi.org\/10.1109\/SWAT.1966.22 10.1109\/SWAT.1966.22","DOI":"10.1109\/SWAT.1966.22"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_16"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3285955"},{"key":"e_1_3_1_58_1","volume-title":"Call-By-Push-Value","author":"Levy Paul Blain","year":"2001","unstructured":"Paul Blain Levy. 2001. Call-By-Push-Value. Ph. D. Dissertation. University of London. https:\/\/www.cs.bham.ac.uk\/~pbl\/ papers\/thesisqmwphd.pdf"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994596"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64437-6_7"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591277"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12925-1_41"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","unstructured":"Martin Odersky and Konstantin L\u00e4ufer. 1996. Putting Type Annotations to Work. In Proceedings of the 23rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. 54\u201367. https:\/\/doi.org\/10.1145\/237721.237729 10.1145\/237721.237729","DOI":"10.1145\/237721.237729"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229062"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1055"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_1_68_1","unstructured":"John C. Reynolds. 1983. Types Abstraction and Parametric Polymorphism. In Information Processing 83 Proceedings of the IFIP 9th World Computer Congress. 513\u2013523."},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15198-2_7"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984008"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2023.11"},{"key":"e_1_3_1_73_1","volume-title":"Some Decision Problems for ML Refinement Types","author":"Skalka Christian","year":"1997","unstructured":"Christian Skalka. 1997. Some Decision Problems for ML Refinement Types. Master\u2019s thesis. Carnegie Mellon University. http:\/\/ceskalka.w3.uvm.edu\/skalka-pubs\/skalka-ms-thesis.ps"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","unstructured":"Marvin H. Solomon. 1978. Type Definitions with Parameters. In Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 31\u201338. https:\/\/doi.org\/10.1145\/512760.512765 10.1145\/512760.512765","DOI":"10.1145\/512760.512765"},{"key":"e_1_3_1_75_1","volume-title":"Polarized Higher-Order Subtyping","author":"Steffen Martin","year":"1999","unstructured":"Martin Steffen. 1999. Polarized Higher-Order Subtyping. Ph. D. Dissertation. University of Erlangen-Nuremberg. https:\/\/martinsteffen.github.io\/assets\/download\/theses\/diss\/diss.pdf"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/S03043975(00)00389-3"},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45294-X_4"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00285-1"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","unstructured":"Peter Thiemann and Vasco T. Vasconcelos. 2016. Context-Free Session Types. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. 462\u2013475. https:\/\/doi.org\/10.1145\/2951913.2951926 10.1145\/2951913.2951926","DOI":"10.1145\/2951913.2951926"},{"key":"e_1_3_1_80_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2950"},{"key":"e_1_3_1_81_1","doi-asserted-by":"publisher","unstructured":"Philip Wadler. 1989. Theorems for Free!. In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture. 347\u2013359. https:\/\/doi.org\/10.1145\/99370.99404 10.1145\/99370.99404","DOI":"10.1145\/99370.99404"},{"key":"e_1_3_1_82_1","first-page":"87","article-title":"Recursive Type Operators Which Are More Than Type Schemes","volume":"8","author":"Wadsworth C. P.","year":"1979","unstructured":"C. P. Wadsworth. 1979. Recursive Type Operators Which Are More Than Type Schemes. Bulletin of the EATCS 8 (1979), 87\u201388.","journal-title":"Bulletin of the EATCS"},{"key":"e_1_3_1_83_1","volume-title":"The Undecidability of Mitchell\u2019s Subtyping Relationship","author":"Wells Joe B.","year":"1995","unstructured":"Joe B. Wells. 1995. The Undecidability of Mitchell\u2019s Subtyping Relationship. Technical Report 95-019. Boston University. http:\/\/www.cs.bu.edu\/ftp\/pub\/jbw\/types\/subtyping-undecidable.ps.gz"},{"key":"e_1_3_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571241"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632932","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632932","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:15Z","timestamp":1751659455000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632932"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":83,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632932"],"URL":"https:\/\/doi.org\/10.1145\/3632932","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}