Dependent Types for JavaScript

Presented as part of the 2013 HCSS conference.

ABSTRACT

Static reasoning for JavaScript is hard due to its combination of challenging features, including run-time type-tests, value-indexed dictionary objects, prototype inheritance, mutable variables, and higher-order functions. In this talk, we describe our statically typed dialect, Dependent JavaScript (DJS), which overcomes many of these obstacles using a combination of new techniques based on refinement types. DJS benefits from the scalability of modern SMT solvers to automatically discharge proof obligations that arise while typechecking JavaScript programs.