{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:08:22Z","timestamp":1750306102067,"version":"3.41.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000038","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":[[2017,10,12]]},"abstract":"<jats:p>Dependent Object Types (DOT) is intended to be a core calculus for modelling Scala. Its distinguishing feature is abstract type members, fields in objects that hold types rather than values. Proving soundness of DOT has been surprisingly challenging, and existing proofs are complicated, and reason about multiple concepts at the same time (e.g. types, values, evaluation). To serve as a core calculus for Scala, DOT should be easy to experiment with and extend, and therefore its soundness proof needs to be easy to modify.<\/jats:p>\n          <jats:p>This paper presents a simple and modular proof strategy for reasoning in DOT. The strategy separates reasoning about types from other concerns. It is centred around a theorem that connects the full DOT type system to a restricted variant in which the challenges and paradoxes caused by abstract type members are eliminated. Almost all reasoning in the proof is done in the intuitive world of this restricted type system. Once we have the necessary results about types, we observe that the other aspects of DOT are mostly standard and can be incorporated into a soundness proof using familiar techniques known from other calculi.<\/jats:p>","DOI":"10.1145\/3133870","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T15:15:45Z","timestamp":1507907745000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["A simple soundness proof for dependent object types"],"prefix":"10.1145","volume":"1","author":[{"given":"Marianna","family":"Rapoport","sequence":"first","affiliation":[{"name":"University of Waterloo, Canada"}]},{"given":"Ifaz","family":"Kabir","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}]},{"given":"Paul","family":"He","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}]},{"given":"Ond\u0159ej","family":"Lhot\u00e1k","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}]}],"member":"320","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_2_1_3_1","volume-title":"Dependent Object Types. In International Workshop on Foundations of Object-Oriented Languages (FOOL","author":"Amin Nada","year":"2012","unstructured":"Nada Amin , Adriaan Moors , and Martin Odersky . 2012 . Dependent Object Types. In International Workshop on Foundations of Object-Oriented Languages (FOOL 2012). Nada Amin, Adriaan Moors, and Martin Odersky. 2012. Dependent Object Types. In International Workshop on Foundations of Object-Oriented Languages (FOOL 2012)."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660216"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984004"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1218563.1218578"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11821069_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_17"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111062"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/74877.74919"},{"key":"e_1_2_1_13_1","volume-title":"International Workshop on Foundations of Object-Oriented Languages (FOOL","author":"Moors Adriaan","year":"2008","unstructured":"Adriaan Moors , Frank Piessens , and Martin Odersky . 2008 . Safe type-level abstraction in Scala . In International Workshop on Foundations of Object-Oriented Languages (FOOL 2008). Adriaan Moors, Frank Piessens, and Martin Odersky. 2008. Safe type-level abstraction in Scala. In International Workshop on Foundations of Object-Oriented Languages (FOOL 2008)."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_10"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094815"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984009"},{"volume-title":"Types and programming languages","author":"Pierce Benjamin C.","key":"e_1_2_1_17_1","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT Press . Benjamin C. Pierce. 2002. Types and programming languages. MIT Press."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3103111.3104036"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.21"},{"key":"e_1_2_1_21_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\/3133870","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133870","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:34Z","timestamp":1750217434000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133870"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":20,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2017,10,12]]}},"alternative-id":["10.1145\/3133870"],"URL":"https:\/\/doi.org\/10.1145\/3133870","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2017,10,12]]},"assertion":[{"value":"2017-10-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}