{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:12:07Z","timestamp":1770282727887,"version":"3.49.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2017,3,6]],"date-time":"2017-03-06T00:00:00Z","timestamp":1488758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-0742736"],"award-info":[{"award-number":["CNS-0742736"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2017,3,31]]},"abstract":"<jats:p>Well-known techniques exist for proving the soundness of subtyping relations with respect to type safety. However, completeness has not been treated with widely applicable techniques, as far as we\u2019re aware.<\/jats:p>\n          <jats:p>This article develops techniques for stating and proving that a subtyping relation is complete with respect to type safety and applies the techniques to the study of iso-recursive subtyping. A new proof technique, induction on failing derivations, is provided that may be useful in other domains as well.<\/jats:p>\n          <jats:p>\n            The common subtyping rules for iso-recursive types\u2014the \u201cAmber rules\u201d\u2014are shown to be incomplete with respect to type safety. That is, there exist iso-recursive types \u03c4\n            <jats:sub>1<\/jats:sub>\n            and \u03c4\n            <jats:sub>2<\/jats:sub>\n            such that \u03c4\n            <jats:sub>1<\/jats:sub>\n            can safely be considered a subtype of \u03c4\n            <jats:sub>2<\/jats:sub>\n            , but \u03c4\n            <jats:sub>1<\/jats:sub>\n            \u2a7d \u03c4\n            <jats:sub>2<\/jats:sub>\n            is not derivable with the Amber rules.\n          <\/jats:p>\n          <jats:p>\n            New, algorithmic rules are defined for subtyping iso-recursive types, and the rules are proved sound and complete with respect to type safety. The fully implemented subtyping algorithm is optimized to run in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>mn<\/jats:italic>\n            ) time, where\n            <jats:italic>m<\/jats:italic>\n            is the number of \u03bc-terms in the types being considered and\n            <jats:italic>n<\/jats:italic>\n            is the size of the types being considered.\n          <\/jats:p>","DOI":"10.1145\/2994596","type":"journal-article","created":{"date-parts":[[2017,3,7]],"date-time":"2017-03-07T19:12:04Z","timestamp":1488913924000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["On Subtyping-Relation Completeness, with an Application to Iso-Recursive Types"],"prefix":"10.1145","volume":"39","author":[{"given":"Jay","family":"Ligatti","sequence":"first","affiliation":[{"name":"University of South Florida"}]},{"given":"Jeremy","family":"Blackburn","sequence":"additional","affiliation":[{"name":"Telefonica Research"}]},{"given":"Michael","family":"Nachtigal","sequence":"additional","affiliation":[{"name":"University of South Florida"}]}],"member":"320","published-online":{"date-parts":[[2017,3,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27375-9_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2379036.2379037"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/21998.22000"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.11.003"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96721"},{"key":"e_1_2_1_9_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of Rewriting and Typed Lambda Calculi (RTA-TLCA\u201914), Gilles Dowek (Ed.)","author":"Dezani-Ciancaglini Mariangiola","unstructured":"Mariangiola Dezani-Ciancaglini and Silvia Ghilezan. 2014. Preciseness of subtyping on intersection and union types. In Proceedings of Rewriting and Typed Lambda Calculi (RTA-TLCA\u201914), Gilles Dowek (Ed.). Lecture Notes in Computer Science, Vol. 8560. Springer International Publishing, 194--207."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004318"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016848.1016872"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Robert Harper. 2013. Practical Foundations for Programming Languages. Retrieved from http:\/\/www.cs.cmu.edu\/&sim;rwh\/plbook\/ Version 1.33 of 05.07.2013 Working Draft.","DOI":"10.5555\/2431407"},{"key":"e_1_2_1_15_1","volume-title":"Turner","author":"Hosoya Haruo","year":"1998","unstructured":"Haruo Hosoya, Benjamin C. Pierce, and David N. Turner. 1998. Datatypes and Subtyping. Manuscript."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053470"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_28"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000657"},{"key":"e_1_2_1_21_1","volume-title":"http:\/\/www.cse.usf.edu\/&sim;ligatti\/projects\/completeness\/sub.sml. (Feb","author":"Ligatti Jay","year":"2016","unstructured":"Jay Ligatti. 2016b. Subtyping-Algorithm Implementation. http:\/\/www.cse.usf.edu\/&sim;ligatti\/projects\/completeness\/sub.sml. (Feb. 2016)."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800528"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs.","author":"Pierik Cees","unstructured":"Cees Pierik and Frank S. De Boer. 2005. On behavioral subtyping and completeness. In Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs."},{"key":"e_1_2_1_27_1","volume-title":"A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60--61","author":"Plotkin Gordon D.","year":"2004","unstructured":"Gordon D. Plotkin. 2004. A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60--61 (2004), 17--139."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/645868.758289"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2002.1.5.c2"},{"key":"e_1_2_1_31_1","volume-title":"Schoonmaker","author":"Stone Christopher A.","year":"2005","unstructured":"Christopher A. Stone and Andrew P. Schoonmaker. 2005. Equational theories with recursive types. (2005). http:\/\/www.cs.hmc.edu\/&sim;stone\/papers\/stone-schoonmaker-long.pdf."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993570"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604187"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_32"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111047"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2994596","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2994596","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2994596","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:39:48Z","timestamp":1750217988000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2994596"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,6]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,3,31]]}},"alternative-id":["10.1145\/2994596"],"URL":"https:\/\/doi.org\/10.1145\/2994596","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,6]]},"assertion":[{"value":"2014-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-03-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}