{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:23:53Z","timestamp":1770276233123,"version":"3.49.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"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":[[2022,10,31]]},"abstract":"<jats:p>\n            Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies currently results in puzzling type errors in most of these languages. Yet this combination of features occurs naturally in many scenarios, such as when manipulating typed ASTs. To support it properly, compilers needs to implement a form of subtyping reconstruction: the ability to reconstruct subtyping information uncovered at runtime during pattern matching. We introduce cDOT, a new calculus in the family of Dependent Object Types (DOT) intended to serve as a formal foundation for subtyping reconstruction. Being descended from pDOT, itself a formal foundation for Scala, cDOT can be used to encode advanced object-oriented features such as generic inheritance, type constructor variance, F-bounded polymorphism, and first-class recursive modules. We demonstrate that subtyping reconstruction subsumes GADTs by encoding \u03bb\n            <jats:sub>\n              2,\n              <jats:italic>G<\/jats:italic>\n              \u00b5\n            <\/jats:sub>\n            , a classical constraint-based GADT calculus, into cDOT.\n          <\/jats:p>","DOI":"10.1145\/3563342","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1526-1555","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoning"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5769-6684","authenticated-orcid":false,"given":"Aleksander","family":"Boruch-Gruszecki","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5539-8245","authenticated-orcid":false,"given":"Rados\u0142aw","family":"Wa\u015bko","sequence":"additional","affiliation":[{"name":"University of Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2089-6767","authenticated-orcid":false,"given":"Yichen","family":"Xu","sequence":"additional","affiliation":[{"name":"Beijing University of Posts and Telecommunications, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8805-0728","authenticated-orcid":false,"given":"Lionel","family":"Parreaux","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"A List of Successes That Can Change the World","author":"Amin Nada","unstructured":"Nada Amin , Samuel Gr\u00fctter , Martin Odersky , Tiark Rompf , and Sandro Stucki . 2016. The Essence of Dependent Object Types . In A List of Successes That Can Change the World . Springer , 249\u2013272. Nada Amin, Samuel Gr\u00fctter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World. Springer, 249\u2013272."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2714064.2660216"},{"key":"e_1_2_1_3_1","unstructured":"Aleksander Boruch-Gruszecki. 2017. Verifying the totality of pattern matching in Scala. Master\u2019s thesis. Wroc\u0142 aw University of Science and Technology. \t\t\t\t  Aleksander Boruch-Gruszecki. 2017. Verifying the totality of pattern matching in Scala. Master\u2019s thesis. Wroc\u0142 aw University of Science and Technology."},{"key":"e_1_2_1_4_1","volume-title":"Yichen Xu, and Lionel Parreaux.","author":"Boruch-Gruszecki Aleksander","year":"2022","unstructured":"Aleksander Boruch-Gruszecki , Rados\u0142 aw Wa\u015bko , Yichen Xu, and Lionel Parreaux. 2022 . A Case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning . https:\/\/doi.org\/10.48550\/arXiv.2209.07427 arxiv:2209.07427. 10.48550\/arXiv.2209.07427 Aleksander Boruch-Gruszecki, Rados\u0142 aw Wa\u015bko, Yichen Xu, and Lionel Parreaux. 2022. A Case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning. https:\/\/doi.org\/10.48550\/arXiv.2209.07427 arxiv:2209.07427."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7079463"},{"key":"e_1_2_1_6_1","volume-title":"Programming in Modula-3: an introduction in programming with style","author":"B\u00f6sz\u00f6rm\u00e9nyi L\u00e1szl\u00f3","unstructured":"L\u00e1szl\u00f3 B\u00f6sz\u00f6rm\u00e9nyi and Carsten Weich . 2012. Programming in Modula-3: an introduction in programming with style . Springer Science & Business Media . L\u00e1szl\u00f3 B\u00f6sz\u00f6rm\u00e9nyi and Carsten Weich. 2012. Programming in Modula-3: an introduction in programming with style. Springer Science & Business Media."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286957"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99392"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409015"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11785477_18"},{"key":"e_1_2_1_12_1","volume-title":"Matching Objects with Patterns. In ECOOP 2007 \u2013 Object-Oriented Programming, Erik Ernst (Ed.). Springer Berlin Heidelberg","author":"Emir Burak","year":"2007","unstructured":"Burak Emir , Martin Odersky , and John Williams . 2007 . Matching Objects with Patterns. In ECOOP 2007 \u2013 Object-Oriented Programming, Erik Ernst (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 273\u2013298. isbn:978-3-540-73589-2 Burak Emir, Martin Odersky, and John Williams. 2007. Matching Objects with Patterns. In ECOOP 2007 \u2013 Object-Oriented Programming, Erik Ernst (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 273\u2013298. isbn:978-3-540-73589-2"},{"key":"e_1_2_1_13_1","volume-title":"Workshop on ML.","author":"Garrigue Jacques","unstructured":"Jacques Garrigue and J. L. Normand . 2011. Adding GADTs to OCaml: The Direct Approach . In Workshop on ML. Jacques Garrigue and J. L. Normand. 2011. Adding GADTs to OCaml: The Direct Approach. In Workshop on ML."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2489837.2489842"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408996"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009871"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199475"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371077"},{"key":"e_1_2_1_19_1","volume-title":"CNRS and contributors","author":"Inria","year":"2021","unstructured":"Inria , CNRS and contributors . 2021 . Extended pattern matching \u2014 Coq 8.13.2 documentation. https:\/\/coq.inria.fr\/distrib\/V8.13.2\/refman\/language\/extensions\/match.html#nested-patterns Inria, CNRS and contributors. 2021. Extended pattern matching \u2014 Coq 8.13.2 documentation. https:\/\/coq.inria.fr\/distrib\/V8.13.2\/refman\/language\/extensions\/match.html#nested-patterns"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784748"},{"key":"e_1_2_1_21_1","volume-title":"On Decidability of Nominal Subtyping with Variance. In International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL\/WOOD).","author":"Kennedy Andrew","unstructured":"Andrew Kennedy and Benjamin C. Pierce . 2007 . On Decidability of Nominal Subtyping with Variance. In International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL\/WOOD). Andrew Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with Variance. In International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL\/WOOD)."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094814"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411304.1411311"},{"key":"e_1_2_1_24_1","unstructured":"Guillaume Martres. 2022. Type-Preserving Compilation of Class-Based Languages. Ph. D. Dissertation. EPFL. Lausanne. \t\t\t\t  Guillaume Martres. 2022. Type-Preserving Compilation of Class-Based Languages. Ph. D. Dissertation. EPFL. Lausanne."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800529"},{"key":"e_1_2_1_26_1","volume-title":"Smith","author":"Nordstr\u00f6m Bengt","year":"1990","unstructured":"Bengt Nordstr\u00f6m , Kent Petersson , and Jan M . Smith . 1990 . Programming in Martin-L\u00f6f\u2019s Type Theory. 200, Oxford University Press Oxford . Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-L\u00f6f\u2019s Type Theory. 200, Oxford University Press Oxford."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-012-9236-6"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3337932.3338813"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5075\/epfl-thesis-10285"},{"key":"e_1_2_1_30_1","volume-title":"Polymorphic Set-Theoretic Types for Functional Languages. Ph. D. Dissertation. Universit\u00e0 di Genova","author":"Petrucciani Tommaso","unstructured":"Tommaso Petrucciani . 2019. Polymorphic Set-Theoretic Types for Functional Languages. Ph. D. Dissertation. Universit\u00e0 di Genova ; Universit\u00e9 Sorbonne Paris Cit\u00e9 \u2013 Universit\u00e9 Paris Diderot . Tommaso Petrucciani. 2019. Polymorphic Set-Theoretic Types for Functional Languages. Ph. D. Dissertation. Universit\u00e0 di Genova ; Universit\u00e9 Sorbonne Paris Cit\u00e9 \u2013 Universit\u00e9 Paris Diderot."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133870"},{"key":"e_1_2_1_33_1","unstructured":"Marianna Rapoport and Ond\u0159ej Lhot\u00e1k. 2019. A Path To DOT: Formalizing Fully-Path-Dependent Types. arXiv:1904.07298 [cs] April arxiv:1904.07298. \t\t\t\t  Marianna Rapoport and Ond\u0159ej Lhot\u00e1k. 2019. A Path To DOT: Formalizing Fully-Path-Dependent Types. arXiv:1904.07298 [cs] April arxiv:1904.07298."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_30"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2887747.2804314"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9022-0"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351248"},{"key":"e_1_2_1_41_1","volume-title":"Formal foundations for Generalized Algebraic Data Types in Scala. Master\u2019s thesis","author":"Wa\u015bko Rados\u0142aw","year":"1973","unstructured":"Rados\u0142aw Wa\u015bko . 2021. Formal foundations for Generalized Algebraic Data Types in Scala. Master\u2019s thesis . University of Warsaw. https :\/\/apd.uw.edu.pl\/diplomas\/ 1973 29\/ Rados\u0142aw Wa\u015bko. 2021. Formal foundations for Generalized Algebraic Data Types in Scala. Master\u2019s thesis. University of Warsaw. https:\/\/apd.uw.edu.pl\/diplomas\/197329\/"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604150"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3486610.3486892"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.294.4"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563342","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563342","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563342"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":45,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563342"],"URL":"https:\/\/doi.org\/10.1145\/3563342","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}