{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:35:02Z","timestamp":1740548102877,"version":"3.38.0"},"reference-count":64,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T00:00:00Z","timestamp":1740528000000},"content-version":"unspecified","delay-in-days":56,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2025]]},"abstract":"Abstract<\/jats:title>\n\t Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala, or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification, and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as decidability<\/jats:italic>, transitivity<\/jats:italic> of subtyping, conservativity<\/jats:italic>, and a sound and complete algorithmic formulation, has been a long-time challenge.<\/jats:p>\n\t This paper shows how to extend \n\t \n\t\t\n\t\t\n$F_{\\le}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula> with iso-recursive types in a new calculus called \n\t \n\t\t\n\t\t\n$F_{\\le}^{\\mu}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula>. \n\t \n\t\t\n\t\t\n$F_{\\le}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula> is a well-known polymorphic calculus with bounded quantification. In \n\t \n\t\t\n\t\t\n$F_{\\le}^{\\mu}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula>, we add iso-recursive types and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. In addition, we use so-called structural<\/jats:italic> folding\/unfolding rules for typing iso-recursive expressions, inspired by the structural unfolding rule proposed by Abadi et al<\/jats:italic>. (1996). The structural rules add expressive power to the more conventional folding\/unfolding rules in the literature, and they enable additional applications. We present several results, including: type soundness; transitivity; the conservativity of \n\t \n\t\t\n\t\t\n$F_{\\le}^{\\mu}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula> over \n\t \n\t\t\n\t\t\n$F_{\\le}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula>; and a sound and complete algorithmic formulation of \n\t \n\t\t\n\t\t\n$F_{\\le}^{\\mu}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula>. We study two variants of \n\t \n\t\t\n\t\t\n$F_{\\le}^{\\mu}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula>. The first one uses an extension of the \n\t \n\t\t\n\t\t\n$\\textrm{kernel}~F_{\\le}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula> (a well-known decidable variant of \n\t \n\t\t\n\t\t\n$F_{\\le}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula>). This extension accepts equivalent<\/jats:italic> rather than equal<\/jats:italic> bounds and is shown to preserve decidable subtyping. The second variant employs the \n\t \n\t\t\n\t\t\n$\\textrm{full}~F_{\\le}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula> rule for bounded quantification and has undecidable subtyping. Moreover, we also study an extension of the kernel version of \n\t \n\t\t\n\t\t\n$F_{\\le}^{\\mu}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula>, called \n\t \n\t\t\n\t\t\n$F_{\\le\\ge}^{\\mu\\wedge}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula>, with a form of intersection types and lower bounded quantification<\/jats:italic>. All the properties from the kernel version of \n\t \n\t\t\n\t\t\n$F_{\\le}^{\\mu}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula> are preserved in \n\t \n\t\t\n\t\t\n$F_{\\le\\ge}^{\\mu\\wedge}$\n<\/jats:tex-math>\n\t <\/jats:alternatives>\n\t <\/jats:inline-formula>. All the results in this paper have been formalized in the Coq theorem prover.<\/jats:p>","DOI":"10.1017\/s0956796825000036","type":"journal-article","created":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T03:43:51Z","timestamp":1740541431000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Recursive subtyping for all"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3046-7085","authenticated-orcid":false,"given":"LITAO","family":"ZHOU","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4170-6160","authenticated-orcid":false,"given":"YAODA","family":"ZHOU","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9894-2462","authenticated-orcid":false,"given":"QIANYONG","family":"WAN","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1846-7210","authenticated-orcid":false,"given":"BRUNO C. D. S.","family":"OLIVEIRA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2025,2,26]]},"reference":[{"key":"S0956796825000036_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99392"},{"key":"S0956796825000036_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00096-5"},{"key":"S0956796825000036_ref14","first-page":"309","article-title":"Coinductive axiomatization of recursive type equality and subtyping","volume":"33","author":"Brandt","year":"1998","journal-title":"Fund. Inf."},{"key":"S0956796825000036_ref15","doi-asserted-by":"publisher","DOI":"10.1002\/j.1096-9942.1995.tb00019.x"},{"key":"S0956796825000036_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_13"},{"key":"S0956796825000036_ref47","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0956796825000036_ref31","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004318"},{"key":"S0956796825000036_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009866"},{"key":"S0956796825000036_ref50","unstructured":"Pottinger, G. (1980) A type assignment for the strongly normalizable \u03bb-terms. In To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561\u2013577."},{"key":"S0956796825000036_ref57","unstructured":"The Coq Development Team. (2021) Coq. v8.13, Available at: https:\/\/coq.inria.fr."},{"key":"S0956796825000036_ref59","doi-asserted-by":"publisher","DOI":"10.1145\/3704869"},{"key":"S0956796825000036_ref64","doi-asserted-by":"publisher","DOI":"10.1145\/3549537"},{"key":"S0956796825000036_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364534"},{"key":"S0956796825000036_ref40","unstructured":"Morris, J. H. (1968) Lambda Calculus Models of Programming Languages. PhD Thesis."},{"key":"S0956796825000036_ref46","unstructured":"Pierce, B. C. (1997) Bounded Quantification with Bottom. CSCI Technical Report 492. Computer Science Department, Indiana University."},{"key":"S0956796825000036_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90042-E"},{"key":"S0956796825000036_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237809"},{"key":"S0956796825000036_ref8","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2802"},{"key":"S0956796825000036_ref17","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2829"},{"key":"S0956796825000036_ref27","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19810270205"},{"key":"S0956796825000036_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"S0956796825000036_ref53","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"S0956796825000036_ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_9"},{"key":"S0956796825000036_ref21","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"S0956796825000036_ref35","unstructured":"INRIA. (1987) OCaml. Available at https:\/\/ocaml.org\/."},{"key":"S0956796825000036_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/2994596"},{"key":"S0956796825000036_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"S0956796825000036_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1018203.1018207"},{"key":"S0956796825000036_ref33","unstructured":"Haskell Development Team. (1990) Haskell. Available at: https:\/\/www.haskell.org\/."},{"key":"S0956796825000036_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/3622809"},{"key":"S0956796825000036_ref56","unstructured":"Scott, D. (1962) A system of functional abstraction. Lectures delivered at University of California, Berkeley, California, USA, 1962\/63."},{"key":"S0956796825000036_ref48","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001040"},{"key":"S0956796825000036_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.11.003"},{"key":"S0956796825000036_ref36","unstructured":"Jeffrey, A. (2001) A symbolic labelled transition system for coinductive subtyping of F \u03bc\u2264 inline1125 types. In 2001 IEEE Conference on Logic and Computer Science (LICS 2001)."},{"key":"S0956796825000036_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263743"},{"key":"S0956796825000036_ref45","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1055"},{"key":"S0956796825000036_ref52","volume-title":"Preliminary Design of the Programming Language Forsythe","author":"Reynolds","year":"1988"},{"key":"S0956796825000036_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"S0956796825000036_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037104"},{"key":"S0956796825000036_ref10","doi-asserted-by":"crossref","unstructured":"Beki\u0107, H. (2005) Definable operations in general algebras, and the theory of automata and flowcharts. In Programming Languages and Their Definition: H. Beki\u010d (1936\u20131982), pp. 30\u201355.","DOI":"10.1007\/BFb0048939"},{"key":"S0956796825000036_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96721"},{"key":"S0956796825000036_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660216"},{"key":"S0956796825000036_ref2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561324"},{"key":"S0956796825000036_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17184-3_38"},{"key":"S0956796825000036_ref7","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-130493"},{"key":"S0956796825000036_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001039"},{"key":"S0956796825000036_ref49","first-page":"112","article-title":"Subtyping and inheritance for categorical datatypes: Preliminary report (type theory and its applications to computer systems)","volume":"1023","author":"Poll","year":"1998","journal-title":"Kyoto Univ. Res. Inf. Repository"},{"key":"S0956796825000036_ref61","doi-asserted-by":"publisher","DOI":"10.1145\/3571241"},{"key":"S0956796825000036_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S0956796825000036_ref58","unstructured":"Wadler, P. (1998) The expression problem. Discussion on the Java Genericity mailing list."},{"key":"S0956796825000036_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"S0956796825000036_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328443"},{"key":"S0956796825000036_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001134"},{"key":"S0956796825000036_ref34","doi-asserted-by":"crossref","unstructured":"Hu, J. & Lhot\u00e1k, O. (2020) Undecidability of D< And its decidable fragments. Proc. ACM Program. Lang. 4(POPL), 1\u201330.","DOI":"10.1145\/3371077"},{"key":"S0956796825000036_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084781"},{"key":"S0956796825000036_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/3371134"},{"key":"S0956796825000036_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/74878.74924"},{"key":"S0956796825000036_ref9","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"S0956796825000036_ref42","unstructured":"Oliveira, B. C. d. S., Cui, S. & Rehman, B. (2020) The duality of subtyping. In 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15\u201317, 2020, Berlin, Germany (Virtual Conference)."},{"key":"S0956796825000036_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177844"},{"key":"S0956796825000036_ref24","doi-asserted-by":"publisher","DOI":"10.2307\/1968337"},{"key":"S0956796825000036_ref30","unstructured":"EPFL. (2021) Scala 3. Available at: https:\/\/www.scala-lang.org\/."},{"key":"S0956796825000036_ref60","doi-asserted-by":"publisher","DOI":"10.1145\/3689718"},{"key":"S0956796825000036_ref63","doi-asserted-by":"publisher","DOI":"10.1145\/3428291"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796825000036","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T03:44:04Z","timestamp":1740541444000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796825000036\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":64,"alternative-id":["S0956796825000036"],"URL":"https:\/\/doi.org\/10.1017\/s0956796825000036","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e8"}}