000227176 001__ 227176
000227176 005__ 20190416055557.0
000227176 0247_ $$2doi$$a10.1145/2983990.2984008
000227176 037__ $$aCONF
000227176 245__ $$aType Soundness for Dependent Object Types’
000227176 269__ $$a2016
000227176 260__ $$c2016
000227176 336__ $$aConference Papers
000227176 520__ $$aScala’s type system unifies aspects of ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, type soundness has only been established for restricted subsets of DOT. In fact, it has been shown that important Scala features such as type refinement or a subtyping relation with lattice structure break at least one key metatheoretic property such as environment narrowing or invertible subtyping transitivity, which are usually required for a type soundness proof. The main contribution of this paper is to demonstrate how, perhaps surprisingly, even though these properties are lost in their full generality, a rich DOT calculus that includes recursive type refinement and a subtyping lattice with intersection types can still be proved sound. The key insight is that subtyping transitivity only needs to be invertible in code paths executed at runtime, with contexts consisting entirely of valid runtime objects, whereas inconsistent subtyping contexts can be permitted for code that is never executed.
000227176 6531_ $$aType Soundness for Dependent Object Types (DOT)
000227176 700__ $$0243345$$g185682$$aRompf, Tiark
000227176 700__ $$0246589$$g164625$$aAmin, Nada
000227176 7112_ $$dNovember 02 - 04, 2016$$cAmsterdam, Netherlands$$aOOPSLA 2016
000227176 773__ $$tProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
000227176 8564_ $$uhttps://infoscience.epfl.ch/record/227176/files/soundness_oopsla16.pdf$$zPostprint$$s315784$$yPostprint
000227176 909C0 $$xU10409$$0252187$$pLAMP
000227176 909CO $$ooai:infoscience.tind.io:227176$$qGLOBAL_SET$$pconf$$pIC
000227176 917Z8 $$x164625
000227176 917Z8 $$x164625
000227176 917Z8 $$x166927
000227176 937__ $$aEPFL-CONF-227176
000227176 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000227176 980__ $$aCONF