English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Scala's type system unifies ML modules, object-oriented, and functionalprogramming. The Dependent Object Types (DOT) family of calculi has beenproposed as a new foundation for Scala and similar languages. Unfortunately, itis not clear how DOT relates to any well-known type systems, and type soundnesshas only been established for very restricted subsets. In fact, important Scalafeatures are known to break at least one key metatheoretic property such asenvironment narrowing or subtyping transitivity, which are usually required fora type soundness proof.  First, and, perhaps surprisingly, we show how rich DOT calculi can still beproved sound. The key insight is that narrowing and subtyping transitivity onlyneed to hold for runtime objects, but not for code that is never executed.Alas, the dominant method of proving type soundness, Wright and Felleisen'ssyntactic approach, is based on term rewriting, which does not a priori make adistinction 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, definitionalinterpreters, implemented in Coq. We present the first mechanized soundnessproof in this style for System F<: and several extensions, including mutablereferences. Our proofs use only simple induction: another surprising result, asthe combination of big-step semantics, mutable references, and polymorphism iscommonly 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 wecollectively call System D. Armed with insights from the definitionalinterpreter semantics, we also show how equivalent small-step semantics andsoundness proofs in Wright-Felleisen-style can be derived for these systems.

From F to DOT: Type Soundness Proofs with Definitional Interpreters