{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:17:14Z","timestamp":1770290234559,"version":"3.49.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>Iso-recursive types are often taken as a type-theoretic model for type recursion as present in many programming languages, e.g., classes in object-oriented languages or algebraic datatypes in functional languages. Their main advantage over an equi-recursive semantics is that they are simpler and algorithmically less expensive, which is an important consideration when the cost of type checking matters, such as for intermediate or low-level code representations, virtual machines, or runtime casts. However, a closer look reveals that iso-recursion cannot, in its standard form, efficiently express essential type system features like mutual recursion or non-uniform recursion. While it has been folklore that mutual recursion and non-uniform type parameterisation can nicely be handled by generalising to higher kinds, this encoding breaks down when combined with subtyping: the classic \u201cAmber\u201d rule for subtyping iso-recursive types is too weak to express mutual recursion without falling back to encodings of quadratic size.<\/jats:p><jats:p>We present a foundational core calculus of iso-recursive types with<jats:italic>declared<\/jats:italic>subtyping that can express both inter- and intra-recursion subtyping without such blowup, including subtyping between constructors of higher or mixed kind. In a second step, we identify a syntactic fragment of this general calculus that allows for more efficient type checking without \u201cdeep\u201d substitutions, by observing that higher-kinded iso-recursive types can be inserted to \u201cguard\u201d against unwanted \u03b2-reductions. This fragment closely resembles the structure of typical nominal subtype systems, but without requiring nominal semantics. It has been used as the basis for a proposed extension of WebAssembly with recursive types.<\/jats:p>","DOI":"10.1145\/3622809","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"347-373","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Mutually Iso-Recursive Subtyping"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3137-3160","authenticated-orcid":false,"given":"Andreas","family":"Rossberg","sequence":"first","affiliation":[{"name":"Independent, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Principles of Programming Languages (POPL)","author":"Abadi Mart\u00edn","unstructured":"Mart\u00edn Abadi , Luca Cardelli , and Ramesh Viswanathan . 1996. An Interpretation of Objects and Object Types . In Principles of Programming Languages (POPL) . ACM Press , 396\u2013409. Mart\u00edn Abadi, Luca Cardelli, and Ramesh Viswanathan. 1996. An Interpretation of Objects and Object Types. In Principles of Programming Languages (POPL). ACM Press, 396\u2013409."},{"key":"e_1_2_1_2_1","volume-title":"Logic in Computer Science","author":"Abadi Mart\u00edn","unstructured":"Mart\u00edn Abadi and Marcelo Fiore . 1996. Syntactic considerations on recursive types . In Logic in Computer Science . IEEE , 242\u2013252. Mart\u00edn Abadi and Marcelo Fiore. 1996. Syntactic considerations on recursive types. In Logic in Computer Science. IEEE, 242\u2013252."},{"key":"e_1_2_1_3_1","first-page":"3","article-title":"Implementing a normalizer using sized heterogeneous types","volume":"19","author":"Abel Andreas","year":"2009","unstructured":"Andreas Abel . 2009 . Implementing a normalizer using sized heterogeneous types . Journal of Functional Programming , 19 , 3 \u2013 4 (2009), 287\u2013310. Andreas Abel. 2009. Implementing a normalizer using sized heterogeneous types. Journal of Functional Programming, 19, 3\u20134 (2009), 287\u2013310.","journal-title":"Journal of Functional Programming"},{"key":"e_1_2_1_4_1","volume-title":"Syntactic Metatheory of Higher-Order Subtyping","author":"Abel Andreas","unstructured":"Andreas Abel and Dulma Rodriguez . 2008. Syntactic Metatheory of Higher-Order Subtyping . In Computer Science Logic, Michael Kaminski and Simone Martini (Eds.). Springer-Verlag , 446\u2013460. Andreas Abel and Dulma Rodriguez. 2008. Syntactic Metatheory of Higher-Order Subtyping. In Computer Science Logic, Michael Kaminski and Simone Martini (Eds.). Springer-Verlag, 446\u2013460."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2802"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2379036.2379037"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2829"},{"key":"e_1_2_1_9_1","volume-title":"Conference on Functional Programming Languages and Computer Architecture. ACM Press, 273\u2013280","author":"Canning Peter","year":"1989","unstructured":"Peter Canning , William Cook , Walter Hill , John Mitchell , and William Olthoff . 1989 . F-bounded polymorphism for object-oriented programming . In Conference on Functional Programming Languages and Computer Architecture. ACM Press, 273\u2013280 . Peter Canning, William Cook, Walter Hill, John Mitchell, and William Olthoff. 1989. F-bounded polymorphism for object-oriented programming. In Conference on Functional Programming Languages and Computer Architecture. ACM Press, 273\u2013280."},{"key":"e_1_2_1_10_1","volume-title":"Amber","author":"Cardelli Luca","unstructured":"Luca Cardelli . 1986. Amber . In Combinators and Functional Programming Languages, Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet (Eds.) (LNCS, 242). Springer-Verlag , 21\u201347. Luca Cardelli. 1986. Amber. In Combinators and Functional Programming Languages, Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet (Eds.) (LNCS, 242). Springer-Verlag, 21\u201347."},{"key":"e_1_2_1_11_1","volume-title":"Theoretical Aspects of Object-Oriented Programming","author":"Cardelli Luca","unstructured":"Luca Cardelli . 1994. Extensible Records in a Pure Calculus of Subtyping . In Theoretical Aspects of Object-Oriented Programming . MIT Press , 373\u2013425. Luca Cardelli. 1994. Extensible Records in a Pure Calculus of Subtyping. In Theoretical Aspects of Object-Oriented Programming. MIT Press, 373\u2013425."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_2_1_13_1","volume-title":"Annual Conference of the European Association for Computer Science Logic (CSL \u201994)","author":"Compagnoni Adriana","year":"1995","unstructured":"Adriana Compagnoni . 1995 . Decidability of higher-order subtyping with intersection types . In Annual Conference of the European Association for Computer Science Logic (CSL \u201994) (LNCS, 933). Springer-Verlag, 46\u201360. Adriana Compagnoni. 1995. Decidability of higher-order subtyping with intersection types. In Annual Conference of the European Association for Computer Science Logic (CSL \u201994) (LNCS, 933). Springer-Verlag, 46\u201360."},{"key":"e_1_2_1_14_1","volume-title":"Principles of Programming Languages (POPL)","author":"Cook William","unstructured":"William Cook , Walter Hill , and Peter Canning . 1989. Inheritance Is Not Subtyping . In Principles of Programming Languages (POPL) . ACM Press , 125\u2013135. William Cook, Walter Hill, and Peter Canning. 1989. Inheritance Is Not Subtyping. In Principles of Programming Languages (POPL). ACM Press, 125\u2013135."},{"key":"e_1_2_1_15_1","volume-title":"What is a recursive module? In Programming Language Design and Implementation (PLDI)","author":"Crary Karl","unstructured":"Karl Crary , Robert Harper , and Sidd Puri . 1999. What is a recursive module? In Programming Language Design and Implementation (PLDI) . ACM Press , Boston, USA. 50\u201363. Karl Crary, Robert Harper, and Sidd Puri. 1999. What is a recursive module? In Programming Language Design and Implementation (PLDI). ACM Press, Boston, USA. 50\u201363."},{"key":"e_1_2_1_16_1","first-page":"80","article-title":"Implementing Statically Typed Object-Oriented Programming","volume":"43","author":"Ducournau Roland","year":"2011","unstructured":"Roland Ducournau . 2011 . Implementing Statically Typed Object-Oriented Programming Languages. Comput. Surveys , 43 , 4 (2011), 80 \u2013 131 . Roland Ducournau. 2011. Implementing Statically Typed Object-Oriented Programming Languages. Comput. Surveys, 43, 4 (2011), 80\u2013131.","journal-title":"Languages. Comput. Surveys"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004318"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2662"},{"key":"e_1_2_1_19_1","volume-title":"Object-oriented Programming, Systems, Languages and Applications (OOPSLA)","author":"Glew Neal","unstructured":"Neal Glew . 2000. An efficient class and object encoding . In Object-oriented Programming, Systems, Languages and Applications (OOPSLA) . ACM Press , 311\u2013324. Neal Glew. 2000. An efficient class and object encoding. In Object-oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press, 311\u2013324."},{"key":"e_1_2_1_20_1","volume-title":"Subtyping for F-Bounded Quantifiers and Equirecursive Types","author":"Glew Neal","unstructured":"Neal Glew . 2012. Subtyping for F-Bounded Quantifiers and Equirecursive Types . Springer-Verlag , 66\u201382. Neal Glew. 2012. Subtyping for F-Bounded Quantifiers and Equirecursive Types. Springer-Verlag, 66\u201382."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1145\/3140587.3062363","article-title":"Bringing the Web up to Speed with WebAssembly","volume":"52","author":"Haas Andreas","year":"2017","unstructured":"Andreas Haas , Andreas Rossberg , Derek Schuff , Ben Titzer , Michael Holman , Dan Gohman , Luke Wagner , Alon Zakai , and JF Bastien . 2017 . Bringing the Web up to Speed with WebAssembly . SIGPLAN Notices , 52 , 6 (2017), 185 \u2013 200 . Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017. Bringing the Web up to Speed with WebAssembly. SIGPLAN Notices, 52, 6 (2017), 185\u2013200.","journal-title":"SIGPLAN Notices"},{"key":"e_1_2_1_22_1","volume-title":"Proof, Language, and Interaction: Essays in Honor of Robin Milner","author":"Harper Robert","unstructured":"Robert Harper and Chris Stone . 2000. A Type-Theoretic Interpretation of Standard ML . In Proof, Language, and Interaction: Essays in Honor of Robin Milner . MIT Press . Robert Harper and Chris Stone. 2000. A Type-Theoretic Interpretation of Standard ML. In Proof, Language, and Interaction: Essays in Honor of Robin Milner. MIT Press."},{"key":"e_1_2_1_23_1","unstructured":"Haruo Hosoya Benjamin Pierce and David Turner. 1998. Datatypes and Subtyping. Haruo Hosoya Benjamin Pierce and David Turner. 1998. Datatypes and Subtyping."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_1_25_1","volume-title":"Principles of Programming Languages (POPL)","author":"Kozen Dexter","unstructured":"Dexter Kozen , Jens Palsberg , and Michael Schwartzbach . 1993. Efficient recursive subtyping . In Principles of Programming Languages (POPL) . ACM Press , Charleston, USA. 419\u2013428. Dexter Kozen, Jens Palsberg, and Michael Schwartzbach. 1993. Efficient recursive subtyping. In Principles of Programming Languages (POPL). ACM Press, Charleston, USA. 419\u2013428."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994596"},{"key":"e_1_2_1_27_1","unstructured":"Sam Lindley Daniel Hillerstr\u00f6m Luna Phipps-Costin Andreas Rossberg Matija Pretnar KC Sivaramakrishnan Arjun Guha and Daan Leijen. 2022. Stack Switching Proposal for WebAssembly. https:\/\/github.com\/WebAssembly\/stack-switching\/ Sam Lindley Daniel Hillerstr\u00f6m Luna Phipps-Costin Andreas Rossberg Matija Pretnar KC Sivaramakrishnan Arjun Guha and Daan Leijen. 2022. Stack Switching Proposal for WebAssembly. https:\/\/github.com\/WebAssembly\/stack-switching\/"},{"key":"e_1_2_1_28_1","unstructured":"Guillaume Martres. 2022. Type-Preserving Compilation of Class-Based Languages. Ph. D. Dissertation. \u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne. Guillaume Martres. 2022. Type-Preserving Compilation of Class-Based Languages. Ph. D. Dissertation. \u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne."},{"key":"e_1_2_1_29_1","volume-title":"International Conference on Functional Programming (ICFP). ACM Press, 28\u201335","author":"Okasaki Chris","year":"1999","unstructured":"Chris Okasaki . 1999 . From fast exponentiation to square matrices: an adventure in types . In International Conference on Functional Programming (ICFP). ACM Press, 28\u201335 . Chris Okasaki. 1999. From fast exponentiation to square matrices: an adventure in types. In International Conference on Functional Programming (ICFP). ACM Press, 28\u201335."},{"key":"e_1_2_1_30_1","volume-title":"Object-oriented Programming, Systems, Languages and Applications (OOPSLA)","author":"Phipps-Costin Luna","unstructured":"Luna Phipps-Costin , Andreas Rossberg , Arjun Guha , Daan Leijen , Daniel Hillerstr\u00f6m , KC Sivaramakrishnan , Matija Pretnar , and Sam Lindley . 2023. Continuing WebAssembly with Effect Handlers . In Object-oriented Programming, Systems, Languages and Applications (OOPSLA) . ACM Press , to appear. Luna Phipps-Costin, Andreas Rossberg, Arjun Guha, Daan Leijen, Daniel Hillerstr\u00f6m, KC Sivaramakrishnan, Matija Pretnar, and Sam Lindley. 2023. Continuing WebAssembly with Effect Handlers. In Object-oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press, to appear."},{"key":"e_1_2_1_31_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin","unstructured":"Benjamin Pierce . 2002. Types and Programming Languages . MIT Press , Boston, USA. Benjamin Pierce. 2002. Types and Programming Languages. MIT Press, Boston, USA."},{"key":"e_1_2_1_32_1","first-page":"1","article-title":"Higher-Order Subtyping","volume":"176","author":"Pierce Benjamin","year":"1997","unstructured":"Benjamin Pierce and Martin Steffen . 1997 . Higher-Order Subtyping . Theoretical Computer Science , 176 , 1 \u2013 2 (1997), 235\u2013282. Benjamin Pierce and Martin Steffen. 1997. Higher-Order Subtyping. Theoretical Computer Science, 176, 1\u20132 (1997), 235\u2013282.","journal-title":"Theoretical Computer Science"},{"key":"e_1_2_1_33_1","volume-title":"Object-Oriented Programming, Systems, Languages and Applications (OOPSLA)","author":"Rompf Tiark","unstructured":"Tiark Rompf and Nada Amin . 2016. Type soundness for dependent object types (DOT) . In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) . ACM Press , 624\u2013641. Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press, 624\u2013641."},{"key":"e_1_2_1_34_1","unstructured":"Andreas Rossberg. 2022. GC Proposal for WebAssembly. https:\/\/github.com\/WebAssembly\/gc\/ Andreas Rossberg. 2022. GC Proposal for WebAssembly. https:\/\/github.com\/WebAssembly\/gc\/"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Andreas Rossberg. 2023. Mutually Iso-recursive Subtyping (Expanded). https:\/\/mpi-sws.org\/ rossberg\/publications\/ Andreas Rossberg. 2023. Mutually Iso-recursive Subtyping (Expanded). https:\/\/mpi-sws.org\/ rossberg\/publications\/","DOI":"10.1145\/3622809"},{"key":"e_1_2_1_36_1","unstructured":"Martin Steffen. 1997. Polarized Higher-Order Subtyping. Ph. D. Dissertation. Universit\u00e4t Erlangen-N\u00fcrnberg. Martin Steffen. 1997. Polarized Higher-Order Subtyping. Ph. D. Dissertation. Universit\u00e4t Erlangen-N\u00fcrnberg."},{"key":"e_1_2_1_37_1","volume-title":"Types for Proofs and Programs (LNCS","volume":"377","author":"Watkins Kevin","year":"2004","unstructured":"Kevin Watkins , Iliano Cervesato , Frank Pfenning , and David Walker . 2004 . A Concurrent Logical Framework: The Propositional Fragment . In Types for Proofs and Programs (LNCS , Vol. 3085). Springer-Verlag, 355\u2013 377 . Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2004. A Concurrent Logical Framework: The Propositional Fragment. In Types for Proofs and Programs (LNCS, Vol. 3085). Springer-Verlag, 355\u2013377."},{"key":"e_1_2_1_38_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\/3622809","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622809","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622809"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":38,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622809"],"URL":"https:\/\/doi.org\/10.1145\/3622809","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}