Dependent Object Types

We propose a new type-theoretic foundation of Scala and languages like it: the Dependent Object Types (DOT) calculus. DOT models Scala’s path-dependent types, abstract type members and its mixture of nominal and structural typing through the use of refinement types. The core formalism makes no attempt to model inheritance and mixin composition. DOT normalizes Scala’s type system by unifying the constructs for type members and by providing classical intersection and union types which simplify greatest lower bound and least upper bound computations. In this paper, we present the DOT calculus, both formally and informally. We also discuss our work-in-progress to prove typesafety of the calculus.

Présenté à:
19th International Workshop on Foundations of Object-Oriented Languages, Tucson, Arizona, USA, October 22, 2012

 Notice créée le 2013-01-10, modifiée le 2019-03-16

Publisher's version:
Télécharger le documentPDF
Lien externe:
Télécharger le documentURL
Évaluer ce document:

Rate this document:
(Pas encore évalué)