000227177 001__ 227177
000227177 005__ 20190416220336.0
000227177 0247_ $$2doi$$a10.1145/3009837.3009866
000227177 02470 $$2ISI$$a000401538900048
000227177 02470 $$2ISI$$a000408311200050
000227177 037__ $$aCONF
000227177 245__ $$aType Soundness Proofs with Definitional Interpreters
000227177 269__ $$a2017
000227177 260__ $$bAssoc Computing Machinery$$c2017$$aNew York
000227177 300__ $$a14
000227177 336__ $$aConference Papers
000227177 520__ $$aWhile type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculus, cannot simultaneously support key metatheoretic properties such as environment narrowing and subtyping transitivity, which are usually required for a type soundness proof. Moreover, Scala and many other realistic languages lack a general substitution property. The first contribution of this paper is to demonstrate how type soundness proofs for advanced, polymorphic, type systems can be carried out with an operational semantics based on high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proofs in this style for System F<: and several extensions, including mutable references. Our proofs use only straightforward induction, which is significant, as the combination of big-step semantics, mutable references, and polymorphism is commonly believed to require coinductive proof techniques. The second main contribution of this paper is to show how DOT-like calculi emerge from straightforward generalizations of the operational aspects of F<:, exposing a rich design space of calculi with path-dependent types inbetween System F and DOT, which we dub the System D Square. By working directly on the target language, definitional interpreters can focus the design space and expose the invariants that actually matter at runtime. Looking at such runtime invariants is an exciting new avenue for type system design.
000227177 6531_ $$aDefinitional interpreters
000227177 6531_ $$atype soundness
000227177 6531_ $$adependent object types
000227177 6531_ $$aDOT
000227177 6531_ $$aScala
000227177 700__ $$0246589$$g164625$$aAmin, Nada
000227177 700__ $$0243345$$g185682$$aRompf, Tiark
000227177 7112_ $$dJanuary 15 - 21, 2017$$cParis, France$$aPOPL 2017
000227177 773__ $$tProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
000227177 8564_ $$uhttps://infoscience.epfl.ch/record/227177/files/big-step.pdf$$zPostprint$$s275100$$yPostprint
000227177 909C0 $$xU10409$$0252187$$pLAMP
000227177 909CO $$ooai:infoscience.tind.io:227177$$qGLOBAL_SET$$pconf$$pIC
000227177 917Z8 $$x164625
000227177 917Z8 $$x166927
000227177 937__ $$aEPFL-CONF-227177
000227177 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000227177 980__ $$aCONF