{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:24Z","timestamp":1750220844425,"version":"3.41.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002790","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002790","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>\n            The Dependent Object Types (DOT) calculus aims to formalize the Scala programming language with a focus on\n            <jats:italic>path-dependent types<\/jats:italic>\n            \u00a0\u2014 types such as\n            <jats:italic>x<\/jats:italic>\n            .\n            <jats:italic>a<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            \u2026\n            <jats:italic>a<\/jats:italic>\n            <jats:sub>\n              <jats:italic>n<\/jats:italic>\n            <\/jats:sub>\n            .\n            <jats:italic>T<\/jats:italic>\n            that depend on the runtime value of a\n            <jats:italic>path<\/jats:italic>\n            <jats:italic>x<\/jats:italic>\n            .\n            <jats:italic>a<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            \u2026\n            <jats:italic>a<\/jats:italic>\n            <jats:sub>\n              <jats:italic>n<\/jats:italic>\n            <\/jats:sub>\n            to an object. Unfortunately, existing formulations of DOT can model only types of the form\n            <jats:italic>x<\/jats:italic>\n            .\n            <jats:italic>A<\/jats:italic>\n            which depend on\n            <jats:italic>variables<\/jats:italic>\n            rather than general paths. This restriction makes it impossible to model nested module dependencies. Nesting small components inside larger ones is a necessary ingredient of a modular, scalable language. DOT\u2019s variable restriction thus undermines its ability to fully formalize a variety of programming-language features including Scala\u2019s module system, family polymorphism, and covariant specialization.\n          <\/jats:p>\n          <jats:p>This paper presents the pDOT calculus, which generalizes DOT to support types that depend on paths of arbitrary length, as well as singleton types to track path equality. We show that naive approaches to add paths to DOT make it inherently unsound, and present necessary conditions for such a calculus to be sound. We discuss the key changes necessary to adapt the techniques of the DOT soundness proofs so that they can be applied to pDOT. Our paper comes with a Coq-mechanized type-safety proof of pDOT. With support for paths of arbitrary length, pDOT can realize DOT\u2019s full potential for formalizing Scala-like calculi.<\/jats:p>","DOI":"10.1145\/3360571","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A path to DOT: formalizing fully path-dependent types"],"prefix":"10.1145","volume":"3","author":[{"given":"Marianna","family":"Rapoport","sequence":"first","affiliation":[{"name":"University of Waterloo, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ond\u0159ej","family":"Lhot\u00e1k","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"volume-title":"A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 249\u2013272.","author":"Amin Nada","key":"e_1_2_2_1_1"},{"volume-title":"Dependent Object Types. In International Workshop on Foundations of Object-Oriented Languages (FOOL","year":"2012","author":"Amin Nada","key":"e_1_2_2_2_1"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009866"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660216"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984004"},{"volume-title":"12th European Conference. 523\u2013549","year":"1998","author":"Bruce Kim B.","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1218563.1218578"},{"volume-title":"31st International Symposium, Slovakia.","year":"2006","author":"Cremet Vincent","key":"e_1_2_2_8_1"},{"volume-title":"Retrieved","year":"2018","author":"Documentation Scala","key":"e_1_2_2_9_1"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604151"},{"volume-title":"Family Polymorphism. In ECOOP 2001 - Object-Oriented Programming, 15th European Conference, Budapest, Hungary, June 18-22, 2001, Proceedings. 303\u2013326","year":"2001","author":"Ernst Erik","key":"e_1_2_2_12_1"},{"volume-title":"Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006","year":"2006","author":"Ernst Erik","key":"e_1_2_2_13_1"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176927"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3241653.3241657"},{"volume-title":"Undecidability of D &lt;: and Its Decidable Fragments. CoRR abs\/1908.05294","year":"2019","author":"Hu Jason","key":"e_1_2_2_16_1"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3241653.3241659"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176926"},{"volume-title":"Virtual Classes: A Powerful Mechanism in Object-Oriented Programming. In Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA\u201989)","year":"1989","author":"Madsen Ole Lehrmann","key":"e_1_2_2_19_1"},{"volume-title":"International Workshop on Foundations of Object-Oriented Languages (FOOL","year":"2008","author":"Moors Adriaan","key":"e_1_2_2_20_1"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_10"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094815"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143228"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133870"},{"volume-title":"A Path To DOT: Formalizing Fully Path-Dependent Types. CoRR abs\/1904.07298","year":"2019","author":"Rapoport Marianna","key":"e_1_2_2_25_1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000205"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450137"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183281"},{"volume-title":"31st European Conference on Object-Oriented Programming, ECOOP 2017","year":"2017","author":"Wang Fei","key":"e_1_2_2_31_1"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360571","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360571","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360571"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":31,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360571"],"URL":"https:\/\/doi.org\/10.1145\/3360571","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}