{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T00:29:25Z","timestamp":1766449765460,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008394","name":"Natur og Univers, Det Frie Forskningsr\u00e5d","doi-asserted-by":"crossref","award":["ModuRes Sapere Aude Advanced Grant"],"award-info":[{"award-number":["ModuRes Sapere Aude Advanced Grant"]}],"id":[{"id":"10.13039\/100008394","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["016.Veni.192.259"],"award-info":[{"award-number":["016.Veni.192.259"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003130","name":"Fonds Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["postdoctoral fellowship (Amin Timany)"],"award-info":[{"award-number":["postdoctoral fellowship (Amin Timany)"]}],"id":[{"id":"10.13039\/501100003130","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":[[2020,8,2]]},"abstract":"<jats:p>The metatheory of Scala\u2019s core type system\u2014the<jats:italic>Dependent Object Types (DOT)<\/jats:italic>calculus\u2014is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and in practice. To address some of these problems, we use a<jats:italic>semantics-first<\/jats:italic>approach to develop a logical relations model for a new version of DOT, called<jats:bold>guarded DOT (gDOT)<\/jats:bold>. Our logical relations model makes use of an abstract form of<jats:italic>step-indexing<\/jats:italic>, as supported by the Iris framework, to model various forms of recursion in gDOT. To demonstrate the expressiveness of gDOT, we show that it handles Scala examples that could not be handled by previous versions of DOT, and prove using our logical relations model that gDOT provides the desired data abstraction. The gDOT type system, its semantic model, its soundness proofs, and all examples in the paper have been mechanized in Coq.<\/jats:p>","DOI":"10.1145\/3408996","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T13:48:02Z","timestamp":1596462482000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris"],"prefix":"10.1145","volume":"4","author":[{"given":"Paolo G.","family":"Giarrusso","sequence":"first","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L\u00e9o","family":"Stefanesco","sequence":"additional","affiliation":[{"name":"IRIF, France \/ University of Paris, France \/ CNRS, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"volume-title":"Rutten","year":"1989","author":"America Pierre","key":"e_1_2_2_2_1"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_2_2_5_1","unstructured":"Nada Amin Adriaan Moors and Martin Odersky. 2012. Dependent object types. In FOOL. Nada Amin Adriaan Moors and Martin Odersky. 2012. Dependent object types. In FOOL."},{"key":"e_1_2_2_6_1","first-page":"666","article-title":"Type soundness proofs with definitional interpreters","author":"Amin Nada","year":"2017","journal-title":"POPL."},{"volume-title":"McAllester","year":"2001","author":"Appel Andrew W.","key":"e_1_2_2_7_1"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1145\/1190216.1190235","article-title":"A very modal model of a modern, major, general type system","author":"Appel Andrew W.","year":"2007","journal-title":"POPL."},{"key":"e_1_2_2_9_1","first-page":"119","article-title":"Stepindexed Kripke models over recursive worlds","author":"Birkedal Lars","year":"2011","journal-title":"POPL."},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Lars Birkedal Kristian St\u00f8vring and Jacob Thamsborg. 2010. The category-theoretic solution of recursive metric-space equations. TCS 411 47 ( 2010 ) 4102-4122. Lars Birkedal Kristian St\u00f8vring and Jacob Thamsborg. 2010. The category-theoretic solution of recursive metric-space equations. TCS 411 47 ( 2010 ) 4102-4122.","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Michael Brandt and Fritz Henglein. 1998. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae 33 4 ( 1998 ) 309-338. Michael Brandt and Fritz Henglein. 1998. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae 33 4 ( 1998 ) 309-338.","DOI":"10.3233\/FI-1998-33401"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1218563.1218578"},{"key":"e_1_2_2_13_1","first-page":"100","article-title":"Modules, abstraction, and parametric polymorphism","author":"Crary Karl","year":"2017","journal-title":"POPL."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301641"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11821069_1"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1145\/1111037.1111062","article-title":"A virtual class calculus","author":"Ernst Erik","year":"2006","journal-title":"POPL."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2020. Compositional Non-Interference for Fine-Grained Concurrent Programs. To appear in S&P' 21. Dan Frumin Robbert Krebbers and Lars Birkedal. 2020. Compositional Non-Interference for Fine-Grained Concurrent Programs. To appear in S&P' 21.","DOI":"10.1109\/SP40001.2021.00003"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_16"},{"volume-title":"\u201cdistributive\u201d? Github issue, https:\/\/web.archive.org\/ web\/20200304175526\/https:\/\/github.com\/lampepfl\/dotty-feature-requests\/issues\/51, archived on","year":"2020","author":"Giarrusso Paolo G.","key":"e_1_2_2_20_1"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3926703."},{"key":"e_1_2_2_22_1","first-page":"123","article-title":"A type-theoretic approach to higher-order modules with sharing","author":"Harper Robert","year":"1994","journal-title":"POPL."},{"volume-title":"Mitchell","year":"1993","author":"Harper Robert","key":"e_1_2_2_23_1"},{"volume-title":"Hu and Ond\u0159ej Lhot\u00e1k","year":"2020","author":"Jason Z.","key":"e_1_2_2_24_1"},{"key":"e_1_2_2_25_1","first-page":"287","article-title":"Pure subtype systems","author":"Hutchins DeLesley S.","year":"2010","journal-title":"POPL."},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2018a. RustBelt: Securing the foundations of the Rust programming language. PACMPL 2 POPL ( 2018 ) 66 : 1-66 : 34. Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2018a. RustBelt: Securing the foundations of the Rust programming language. PACMPL 2 POPL ( 2018 ) 66 : 1-66 : 34.","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2020. Safe systems programming in Rust: The promise and the challenge. To appear in CACM. Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2020. Safe systems programming in Rust: The promise and the challenge. To appear in CACM.","DOI":"10.1145\/3418295"},{"key":"e_1_2_2_28_1","first-page":"256","article-title":"Higher-order ghost state","author":"Jung Ralf","year":"2016","journal-title":"ICFP."},{"key":"e_1_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP 28 ( 2018 ) e20. Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP 28 ( 2018 ) e20.","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"volume-title":"DOT: Scaling DOT with mutation and constructors. In SCALA@ICFP. 40-50.","year":"2018","author":"Kabir Ifaz","key":"e_1_2_2_31_1"},{"key":"e_1_2_2_32_1","first-page":"86","article-title":"Dependent intersection: A new way of defining records in type theory","author":"Kopylov Alexei","year":"2003","journal-title":"LICS."},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: A general extensible modal framework for interactive proofs in separation logic. PACMPL 2 ICFP ( 2018 ) 77 : 1-77 : 30. Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: A general extensible modal framework for interactive proofs in separation logic. PACMPL 2 ICFP ( 2018 ) 77 : 1-77 : 30.","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_35_1","first-page":"205","article-title":"Interactive proofs in higher-order concurrent separation logic","author":"Krebbers Robbert","year":"2017","journal-title":"POPL."},{"key":"e_1_2_2_36_1","first-page":"218","article-title":"A relational model of types-and-efects in higher-order concurrent separation logic","author":"Krogh-Jespersen Morten","year":"2017","journal-title":"POPL."},{"key":"e_1_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Robin Milner. 1978. A theory of type polymorphism in programming. JCSS 17 3 ( 1978 ) 348-375. Robin Milner. 1978. A theory of type polymorphism in programming. JCSS 17 3 ( 1978 ) 348-375.","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_38_1","first-page":"255","article-title":"A Modality for Recursion","author":"Nakano Hiroshi","year":"2000","journal-title":"LICS."},{"key":"e_1_2_2_39_1","doi-asserted-by":"crossref","unstructured":"Abel Nieto. 2017. Towards algorithmic typing for DOT (short paper). In SCALA@SPLASH. 2-7. Abel Nieto. 2017. Towards algorithmic typing for DOT (short paper). In SCALA@SPLASH. 2-7.","DOI":"10.1145\/3136000.3136003"},{"volume-title":"DOT with higher-kinded types. Github discussion, https:\/\/web.archive.org\/web\/20200304175613\/https: \/\/gist.github. com\/odersky\/36aee4b7fe6716d1016ed37051caae95, archived on","year":"2020","author":"Odersky Martin","key":"e_1_2_2_40_1"},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"Martin Odersky Guillaume Martres and Dmitry Petrashko. 2016. Implementing higher-kinded types in Dotty. In SCALA@SPLASH. 51-60. Martin Odersky Guillaume Martres and Dmitry Petrashko. 2016. Implementing higher-kinded types in Dotty. In SCALA@SPLASH. 51-60.","DOI":"10.1145\/2998392.2998400"},{"key":"e_1_2_2_42_1","doi-asserted-by":"crossref","unstructured":"Marianna Rapoport Ifaz Kabir Paul He and Ond\u0159ej Lhot\u00e1k. 2017. A simple soundness proof for dependent object types. PACMPL 1 OOPSLA ( 2017 ) 46 : 1-46 : 27. Marianna Rapoport Ifaz Kabir Paul He and Ond\u0159ej Lhot\u00e1k. 2017. A simple soundness proof for dependent object types. PACMPL 1 OOPSLA ( 2017 ) 46 : 1-46 : 27.","DOI":"10.1145\/3133870"},{"key":"e_1_2_2_44_1","doi-asserted-by":"crossref","unstructured":"Marianna Rapoport and Ond\u0159ej Lhot\u00e1k. 2019. A path to DOT: formalizing fully path-dependent types. PACMPL 3 OOPSLA ( 2019 ) 145 : 1-145 : 29. Marianna Rapoport and Ond\u0159ej Lhot\u00e1k. 2019. A path to DOT: formalizing fully path-dependent types. PACMPL 3 OOPSLA ( 2019 ) 145 : 1-145 : 29.","DOI":"10.1145\/3360571"},{"key":"e_1_2_2_45_1","first-page":"624","article-title":"Type soundness for dependent object types (DOT)","author":"Rompf Tiark","year":"2016","journal-title":"OOPSLA."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"e_1_2_2_47_1","unstructured":"Paula Severi. 2019. A light modality for recursion. LMCS 15 1 ( 2019 ). Paula Severi. 2019. A light modality for recursion. LMCS 15 1 ( 2019 )."},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1145\/3293880.3294101","article-title":"Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions","author":"Stark Kathrin","year":"2019","journal-title":"CPP."},{"volume-title":"DOT with higher-kinded types-A sketch. Github discussion, https:\/\/web.archive.org\/web\/ 20200304175148\/https:\/\/gist.github. com\/sstucki\/3fa46d2c4ce6f54dc61c3d33fc898098, archived on","year":"2020","author":"Stucki Sandro","key":"e_1_2_2_49_1"},{"key":"e_1_2_2_51_1","doi-asserted-by":"crossref","unstructured":"David Swasey Deepak Garg and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. PACMPL 1 OOPSLA ( 2017 ) 89 : 1-89 : 26. David Swasey Deepak Garg and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. PACMPL 1 OOPSLA ( 2017 ) 89 : 1-89 : 26.","DOI":"10.1145\/3133913"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_53_1","doi-asserted-by":"crossref","unstructured":"Amin Timany L\u00e9o Stefanesco Morten Krogh-Jespersen and Lars Birkedal. 2018. A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST. PACMPL 2 POPL ( 2018 ) 64 : 1-64 : 28. Amin Timany L\u00e9o Stefanesco Morten Krogh-Jespersen and Lars Birkedal. 2018. A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST. PACMPL 2 POPL ( 2018 ) 64 : 1-64 : 28.","DOI":"10.1145\/3158152"},{"key":"e_1_2_2_54_1","volume-title":"ECOOP (LIPIcs","volume":"74","author":"Wang Fei","year":"2017"},{"volume-title":"d. S. Oliveira","year":"2017","author":"Yang Yanpeng","key":"e_1_2_2_55_1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408996","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408996","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:59Z","timestamp":1750193279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408996"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":51,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3408996"],"URL":"https:\/\/doi.org\/10.1145\/3408996","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}