Precise Type Checking for JavaScript

Dynamic scripting languages have recently experienced a dramatic growth. JavaScript in particular is one of the main technologies powering the web. As web applications grow in complexity so does the need for means to guarantee their correctness. Testing has been a valuable ally, but falls short with respect to program coverage and formal correctness guarantees. To complement this approach we propose static type-based analysis. Our goals are early bug detection, code intelligence for editors and verifying specifications; all with modest annotation effort from the developer. The biggest challenge is the dynamic nature of JavaScript: overloaded functions, closures, and mutability both at the stack and heap level.In this dissertation, we describe our solutions to the problem of type checking JavaScript in three main contributions. First, we present the constraint-based type inference engine powering Flow, a static type checker for JavaScript. Here constraint generation accounts for uses of values throughout the program, and constraint propagation corresponds to the notion of subtyping. Detecting bugs amounts to finding inconsistencies in the propagated constraint set. We present a formal core that supports type refinement based on runtime tests, higher-order functions, mutable variables and capture-by-reference, and prove it sound. Second, we tackle the problem of value-based overloading, where functions dynamically reflect upon and behave according to the types of their arguments. We present a novel two-phased approach to type checking that breaks the circular dependency between value and type reasoning in heavily dynamic languages. Our technique enables the straightforward composition of simple type checkers with program logics. Leveraging this advancement is our third contribution, Refined TypeScript (RSC), a refinement type system for TypeScript that enables static verification of higher-order, imperative programs. We develop a formal core of RSC that delineates the interaction between refinement types and mutability, both on local variables and objects. The core is proven sound and extended to account for features of real-world TypeScript programs. We evaluate our checker on a set of benchmarks, including parts of the Octane benchmarks and the TypeScript compiler