Bringing Verification to Scala through Dependent Refinement Types

EDIC candidacy exam
Exam president: Prof. Christoph Koch
Thesis advisor: Prof. Viktor Kuncak
Co-examiner: Prof. Martin Odersky

Abstract
Despite numerous advances in type systems, program analysis and model checking, the verification of software artifacts is still the exception rather than the rule.
Dependent refinement types have emerged as a verification technique that allows for expressive specifications, but retains the familiar user interface of types.
In recent work the checking of such types has been delegated to SMT solvers, allowing programmers to largely automate the verification of simple program properties, while aiding them in proving more complex ones.

In this report we survey dependent refinement types in the functional setting and consequently propose how Scala can evolve to support them.
We start out by introducing two concrete incarnations of dependent refinement types, LiquidTypes and the type system of F*.
We then discuss how their techniques may be applied to languages featuring rich, user-defined subtyping relations and object-oriented programming, such as in Scala.
To this end, we also explore the extent to which type inference remains feasible in the presence of subtyping.
Drawing on these insights, we finally present our research proposal for dependent refinement types in Scala.

Background papers
Liquid Types; Rondon et al.
Dependent Types and Multi-monadic Effects in F*; Swamy et al.
Type Inference with Simple Subtypes; Mitchell.