Type-Preserving Compilation of Class-Based Languages

TL;DR

This paper develops a series of calculi to model Scala and presents a type-preserving compilation scheme into DOT, addressing the impedance mismatch between class-based Scala and structural DOT types.

Contribution

It introduces a systematic, type-preserving compilation method from Scala-like calculi into DOT, including necessary extensions to DOT for soundness.

Findings

Successful compilation schemes for Scala into DOT

Extensions to DOT to handle class-based features

Formal proofs of type preservation

Abstract

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is not enough to declare a particular subset of the language as sound. While a few examples of Scala snippets have been manually translated into DOT, no systematic compilation scheme has been presented so far. In this thesis we develop a series of calculi of increasing complexity to model Scala and present a type-preserving compilation scheme from each of these calculus into DOT. Along the way, we develop some necessary extensions to DOT.