E-resources
Open access
-
Rompf, Tiark; Amin, Nada
arXiv.org, 02/2016Paper, Journal Article
Scala's type system unifies ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new foundation for Scala and similar languages. Unfortunately, it is not clear how DOT relates to any well-known type systems, and type soundness has only been established for very restricted subsets. In fact, important Scala features are known to break at least one key metatheoretic property such as environment narrowing or subtyping transitivity, which are usually required for a type soundness proof. First, and, perhaps surprisingly, we show how rich DOT calculi can still be proved sound. The key insight is that narrowing and subtyping transitivity only need to hold for runtime objects, but not for code that is never executed. Alas, the dominant method of proving type soundness, Wright and Felleisen's syntactic approach, is based on term rewriting, which does not a priori make a distinction between runtime and type assignment time. Second, we demonstrate how type soundness can be proved for advanced, polymorphic, type systems with respect to high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proof in this style for System F<: and several extensions, including mutable references. Our proofs use only simple induction: another surprising result, as the combination of big-step semantics, mutable references, and polymorphism is commonly believed to require co-inductive proof techniques. Third, we show how DOT-like calculi emerge as generalizations of F<:, exposing a rich design space of calculi with path-dependent types which we collectively call System D. Armed with insights from the definitional interpreter semantics, we also show how equivalent small-step semantics and soundness proofs in Wright-Felleisen-style can be derived for these systems.
![loading ... loading ...](themes/default/img/ajax-loading.gif)
Shelf entry
Permalink
- URL:
Impact factor
Access to the JCR database is permitted only to users from Slovenia. Your current IP address is not on the list of IP addresses with access permission, and authentication with the relevant AAI accout is required.
Year | Impact factor | Edition | Category | Classification | ||||
---|---|---|---|---|---|---|---|---|
JCR | SNIP | JCR | SNIP | JCR | SNIP | JCR | SNIP |
Select the library membership card:
If the library membership card is not in the list,
add a new one.
DRS, in which the journal is indexed
Database name | Field | Year |
---|
Links to authors' personal bibliographies | Links to information on researchers in the SICRIS system |
---|
Source: Personal bibliographies
and: SICRIS
The material is available in full text. If you wish to order the material anyway, click the Continue button.