[PRL] [1510.05216] From F to DOT: Type Soundness Proofs with Definitional Interpreters

Mitchell Wand wand at ccs.neu.edu
Tue Oct 20 07:16:51 EDT 2015


Your morning link: Not read, but sounds neat....

>From F to DOT: Type Soundness Proofs with Definitional Interpreters

Tiark Rompf, Nada Amin
(Submitted on 18 Oct 2015)
Scala's type system unifies aspects of ML-style module systems,
object-oriented, and functional programming paradigms. The DOT (Dependent
Object Types) 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 a very restricted subset of DOT
(muDOT), and it has been shown that adding important Scala features such as
type refinement or extending subtyping to a lattice breaks at least one key
metatheoretic property such as narrowing or subtyping transitivity, which
are usually required for a type soundness proof.
The first main contribution of this paper is to demonstrate how, perhaps
surprisingly, even though these properties are lost in their full
generality, a richer DOT calculus that includes both type refinement and a
subtyping lattice with intersection types 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 make an adequate
distinction between runtime and type assignment time.
The second main 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
proof for System F<: based on a definitional interpreter. We discuss the
challenges that arise in this setting, in particular due to abstract types,
and we illustrate in detail how DOT-like calculi emerge from
straightforward generalizations of the operational aspects of F<:.
http://arxiv.org/abs/1510.05216
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the PRL mailing list