Nested Refinement Types for JavaScript

Decades of research on type systems have led to advances in the kinds of programming features that can be reasoned about and the kinds of errors that can be prevented. Nevertheless, the programming idioms in untyped, or dynamic, languages make heavy use of features --- run-time type tests, mutable objects indexed by dynamically computed keys, prototype inheritance, and higher-order functions --- that are beyond the reach of prior type systems. Because of the rising popularity of languages like JavaScript and Python, as well as the addition of dynamic features to statically typed languages, techniques for reasoning about untyped languages are potentially very valuable. In this dissertation, we present Dependent JavaScript, a statically typed dialect of the imperative, object-oriented, dynamic language. Our system builds on refinement types, which augment traditional syntactic types with logical predicates to enable finer-grained reasoning. We make several contributions to overcome limitations in prior refinement type systems that prevent precise reasoning about idiomatic code in dynamic languages. First, we present nested refinement types, where the typing relation is itself a predicate in the refinement logic in order to specify types for programs that manipulate objects with dynamically computed keys. By carefully coordinating SMT-based logical implication with syntactic techniques, nested refinement subtyping enables reasoning about such programs without resorting to a complex refinement logic. Second, we present a formulation of flow-sensitive refinement types to retain the precision of refinement types despite the presence of mutable variables. Finally, we present a refinement type encoding called heap unrolling to reason about the semantics of prototype-based inheritance, again, without resorting to a complex refinement logic. To demonstrate how these novel techniques combine, we implement a type checker for Dependent JavaScript and evaluate its expressiveness on a set of small, but challenging, JavaScript examples adapted from several benchmark