000227018 001__ 227018
000227018 005__ 20190317000653.0
000227018 0247_ $$2doi$$a10.1145/2983990.2984008
000227018 022__ $$a0362-1340
000227018 02470 $$2ISI$$a000393581000036
000227018 037__ $$aCONF
000227018 245__ $$aType Soundness for Dependent Object Types (DOT)
000227018 269__ $$a2016
000227018 260__ $$bAssoc Computing Machinery$$c2016$$aNew York
000227018 300__ $$a18
000227018 336__ $$aConference Papers
000227018 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 run time, with contexts consisting entirely of valid runtime objects, whereas inconsistent subtyping contexts can be permitted for code that is never executed.
000227018 6531_ $$adependent object types
000227018 6531_ $$aDOT
000227018 6531_ $$aScala
000227018 6531_ $$asoundness
000227018 700__ $$0243345$$g185682$$uPurdue Univ, W Lafayette, IN 47907 USA$$aRompf, Tiark
000227018 700__ $$aAmin, Nada$$g164625$$0246589
000227018 7112_ $$dNOV 02-04, 2016$$cAmsterdam, NETHERLANDS$$aACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
000227018 773__ $$j51$$tAcm Sigplan Notices$$k10$$q624-641
000227018 8564_ $$uhttps://infoscience.epfl.ch/record/227018/files/soundness_oopsla16.pdf$$zPostprint$$s315784$$yPostprint
000227018 909C0 $$xU10409$$0252187$$pLAMP
000227018 909CO $$qGLOBAL_SET$$pconf$$ooai:infoscience.tind.io:227018$$pIC
000227018 917Z8 $$x164625
000227018 937__ $$aEPFL-CONF-227018
000227018 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000227018 980__ $$aCONF