{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T03:12:54Z","timestamp":1770347574280,"version":"3.49.0"},"reference-count":58,"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":"Hong Kong Research Grant Council","award":["17209821"],"award-info":[{"award-number":["17209821"]}]}],"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>Many programming languages need to check whether two recursive types are in a subtyping relation. Traditionally recursive types are modelled in two different ways: equi- or iso- recursive types. While efficient algorithms for subtyping equi-recursive types are well studied for simple type systems, efficient algorithms for iso-recursive subtyping remain understudied.<\/jats:p>\n                  <jats:p>\n                    In this paper we present\n                    <jats:monospace>QuickSub<\/jats:monospace>\n                    : an efficient and simple to implement algorithm for iso-recursive subtyping.\n                    <jats:monospace>QuickSub<\/jats:monospace>\n                    has the same expressive power as the well-known iso-recursive Amber rules. The worst case complexity of\n                    <jats:monospace>QuickSub<\/jats:monospace>\n                    is\n                    <jats:italic toggle=\"yes\">O<\/jats:italic>\n                    (\n                    <jats:italic toggle=\"yes\">nm<\/jats:italic>\n                    ), where\n                    <jats:italic toggle=\"yes\">m<\/jats:italic>\n                    is the size of the type and\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    is the number of recursive binders. However, in practice, the algorithm is\n                    <jats:italic toggle=\"yes\">nearly linear<\/jats:italic>\n                    with the worst case being hard to reach. Consequently, in many common cases,\n                    <jats:monospace>QuickSub<\/jats:monospace>\n                    can be several times faster than alternative algorithms. We validate the efficiency of\n                    <jats:monospace>QuickSub<\/jats:monospace>\n                    with an empirical evaluation comparing it to existing equi-recursive and iso-recursive subtyping algorithms. We prove the correctness of the algorithm and formalize a simple calculus with recursive subtyping and records. For this calculus we also show how type soundness can be proved using\n                    <jats:monospace>QuickSub<\/jats:monospace>\n                    . All the results have been formalized and proved in the Coq proof assistant.\n                  <\/jats:p>","DOI":"10.1145\/3704869","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"954-985","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["QuickSub: Efficient Iso-Recursive Subtyping"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3046-7085","authenticated-orcid":false,"given":"Litao","family":"Zhou","sequence":"first","affiliation":[{"name":"University of Hong Kong, Hong Kong, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1846-7210","authenticated-orcid":false,"given":"Bruno C. d. S.","family":"Oliveira","sequence":"additional","affiliation":[{"name":"University of Hong Kong, Hong Kong, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561324"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009866"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325727"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-130493"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1998-33401"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17184-3"},{"key":"e_1_3_2_12_1","article-title":"Digital Equipment Corporation Systems Research Center","author":"Cardelli Luca","year":"1993","unstructured":"Luca Cardelli . 1993. An implementation of F<. Digital Equipment Corporation Systems Research Center.","journal-title":"An implementation of F<"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90020-3"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599437"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643135.2643138"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_11"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.11.003"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015737"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2024. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.11551307 10.5281\/zenodo.11551307","DOI":"10.5281\/zenodo.11551307"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301641"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13321-3_8"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70216-7"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Henry DeYoung Andreia Mordido Frank Pfenning and Ankush Das. 2024. Parametric Subtyping for Structural Parametric Polymorphism. 8 POPL (2024). https:\/\/doi.org\/10.1145\/3632932 10.1145\/3632932","DOI":"10.1145\/3632932"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1087953"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.21236\/ada460172"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/586088.586093"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004318"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037104"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316576892"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199482"},{"key":"e_1_3_2_35_1","article-title":"Datatypes and subtyping","author":"Hosoya Haruo","year":"1998","unstructured":"Haruo Hosoya, Benjamin C Pierce, David N Turner, et al. 1998. Datatypes and subtyping. Unpublished manuscript. Available http:\/\/www.cis.upenn.edu\/bcpierce\/papers\/index.html (1998).","journal-title":"Unpublished manuscript"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932508"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141540"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158700"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2015.174"},{"key":"e_1_3_2_40_1","article-title":"The OCaml System, Release 4.12","author":"Leroy Xavier","year":"2021","unstructured":"Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier R\u00e9my, and J\u00e9r\u00f4me Vouillon. 2021. The OCaml System, Release 4.12, Documentation and User's Manual. https:\/\/ocaml.org\/manual\/4.12\/index.html Accessed: 2024-07-06.","journal-title":"Documentation and User's Manual."},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994596"},{"key":"e_1_3_2_42_1","unstructured":"James H Morris . 1968. Lambda calculus models of programming languages. (1968)."},{"key":"e_1_3_2_43_1","unstructured":"Ulf Norell . 2007. Towards a practical programming language basedon dependent type theory. Ph. D. Dissertation. Chalmers University of Technology."},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434302"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_2_47_1","article-title":"Research Report RR-3483","author":"Pottier Fran\u00e7ois","year":"1998","unstructured":"Fran\u00e7ois Pottier . 1998. Type Inference in the Presence of Subtyping: from Theory to Practice. Research Report RR-3483. INRIA. https:\/\/inria.hal.science\/inria-00073205","journal-title":"Type Inference in the Presence of Subtyping: from Theory to Practice"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622809"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507644"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_21"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034811"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1996-281213"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","unstructured":"Litao Zhou and Bruno C. d. S. Oliveira. 2024. Quick Sub: Efficient Iso-Recursive Subtyping (Artifact). https:\/\/doi.org\/10.5281\/zenodo.13906402 10.5281\/zenodo.13906402","DOI":"10.5281\/zenodo.13906402"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689718"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571241"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_9"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428216"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3549537"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704869","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704869","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:45Z","timestamp":1770200265000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704869"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":58,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704869"],"URL":"https:\/\/doi.org\/10.1145\/3704869","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-10","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"}}]}}