Dependent Types for JavaScript
Ravi ChughDavid Herman

Ranjit Jhala

University of California, San Diegorchugh@cs.ucsd.edu

Mozilla Researchdherman@mozilla.com

University of California, San Diegojhala@cs.ucsd.edu

Abstract
We present Dependent JavaScript (DJS), a statically typed
dialect of the imperative, object-oriented, dynamic language.
DJS supports the particularly challenging features such as
run-time type-tests, higher-order functions, extensible objects, prototype inheritance, and arrays through a combination of nested refinement types, strong updates to the heap,
and heap unrolling to precisely track prototype hierarchies.
With our implementation of DJS, we demonstrate that thetype system is expressive enough to reason about a varietyof tricky idioms found in small examples drawn from several
sources, including the popular book JavaScript: The Good
Parts and the SunSpider benchmark suite.
Categories and Subject Descriptors D.3.3 [Programming
Languages]: Language Constructs and Features – Inheritance, Polymorphism; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs – Logics of Programs
Keywords Refinement Types, JavaScript, Strong Updates,
Prototype Inheritance, Arrays

1.

Introduction

Dynamic languages like JavaScript, Python, and Ruby arewidely popular for building both client and server applications, in large part because they provide powerful sets offeatures — run-time type tests, mutable variables, extensible objects, and higher-order functions. But as applications
grow, the lack of static typing makes it difficult to achieve
reliability, security, maintainability, and performance. In response, several authors have proposed type systems which
provide static checking for various subsets of dynamic languages [5, 16, 22, 23, 30, 36].
Recently, we developed System D [9], a core calculus
for dynamic languages that supports the above dynamic id-

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
OOPSLA’12, October 19–26, 2012, Tucson, Arizona, USA.
Copyright © 2012 ACM 978-1-4503-1561-6/12/10. . . $10.00

ioms but in a purely functional setting. The main insight inSystem D is to dependently type all values with formulas
drawn from an SMT-decidable refinement logic. We use an
SMT solver to reason about the properties it tracks well,namely, control-flow invariants and dictionaries with dynamic keys that bind scalar values. But to describe dynamic
keys that bind rich values like functions, System D encodes
function types as logical terms and nests the typing relation
as an uninterpreted predicate within the logic. By dividing
work between syntactic subtyping and SMT-based validity
checking, the calculus supports fully automatic checking ofdynamic features like run-time type tests, value-indexed dictionaries, higher-order functions, and polymorphism.
In this paper, we scale up the System D calculus to
Dependent JavaScript (abbreviated to DJS), an explicitly
typed dialect of a real-world, imperative, object-oriented,
dynamic language. We bridge the vast gap between System D
and JavaScript in three steps.
Step 1: Imperative Updates. The types of variables in
JavaScript are routinely “changed” either by assignment or
by incrementally adding or removing fields to objects boundto variables. The presence of mutation makes it challenging
to assign precise types to variables, and the standard methodof assigning a single “invariant” reference type that overapproximates all values held by the variable is useless in the
JavaScript setting. We overcome this challenge by extending
our calculus with flow-sensitive heap types (in the style of[2, 12, 15, 31, 32]) which allow the system to precisely track
the heap location each variable refers to as well as aliasing relationships, thereby enabling strong updates throughmutable variables. Our formulation of flow-sensitive heaps
combined with higher-order functions and refinement types
is novel, and allows DJS to express precise pre- and postconditions of heaps, as in separation logic [17].
Step 2: Prototype Inheritance. Each JavaScript object
maintains an implicit link to the “prototype” object fromwhich it derives. To resolve a key lookup from an object at
run-time, JavaScript transitively follows its prototype links
until either the key is found or the root is reached without
success. Thus, unlike in class-based languages, inheritance
relationships are computed at run-time rather than provided
as declarative specifications. The semantics of prototypes ischallenging for static typing, because to track the type of a
key binding, the system must statically reason about a potentially unbounded number of prototype links! In DJS, we
solve this problem with a novel decomposition of the heap
into a “shallow” part, for which we precisely track a finite
number of prototype links, and a “deep” part, for which we
do not have precise information, represented abstractly via
a logical heap variable. We unroll prototype hierarchies inshallow heaps to precisely model the semantics of object operations, and we use uninterpreted heap predicates to reason
abstractly about deep parts. In this way, we reduce the reasoning about unbounded, imperative, prototype hierarchies
to the underlying decidable, first-order, refinement logic.
Step 3: Arrays. JavaScript arrays are simply objects whose
keys are string representations of integers. Arrays are commonly used both as heterogeneous tuples (that have a fixed
number of elements of different types) as well as homogeneous collections (that have an unbounded number of elements of the same type). The overloaded use of arrays, together with the fact that arrays are otherwise syntacticallyindistinguishable and have the same prototype-based semantics as non-array objects, makes it hard to statically reason
about the very different ways in which they are used. In DJS,
we use nested refinements to address the problem neatly by
uniformly encoding tuples and collections with refinement
predicates, and by using intersection types that simultaneous encode the semantics of tuples, collections, and objects.
Expressiveness. We have implemented DJS (available atravichugh.com/djs) and demonstrated its expressivenessby checking a variety of properties found in small but subtle examples drawn from a variety of sources, including the
popular book JavaScript: The Good Parts [10] and the SunSpider benchmark suite [34]. Our experiments show thatseveral examples simultaneously require the gamut of features in DJS, but that many examples conform to recurring
patterns that rely on particular aspects of the type system.
We identify several ways in which future work can handle
these patterns more specifically in order to reduce the annotation burden and performance for common cases, while
falling back to the full expressiveness of DJS in general.
Thus, we believe that DJS provides a significant step towards
truly retrofitting JavaScript with a practical type system.

2.

Overview

program.js

basics.dref
objects.dref
prelude.dref

DJS	  Desugarer	
  program.dref

System	
  !D	
  
Type	
  
Checker	  Figure 1. Architecture of DJS
As λJS is a core language with well-understood semantics
and proof techniques, the translation paves a path to a typed
dialect of JavaScript: define a type system for the core language and then type check desugared JavaScript programs.
We take this path by developing System !D (pronounced“D-ref”), a new calculus based on λJS . Although the operational semantics of System !D is straightforward, the dynamic features of the language ensure that building a typesystem expressive enough to support desugared JavaScript
idioms is not. We solve this problem by scaling the purely
functional technique of nested refinement types up to the imperative, object-oriented, setting of real-world JavaScript.
Figure 1 depicts the architecture of our approach: we
desugar a Dependent JavaScript (DJS) file program.js to
the System !D file program.dref, which is analyzed by thetype checker along with a standard prelude comprising three
files (basics.dref, objects.dref, and prelude.dref)that model JavaScript semantics.
Terminology. JavaScript has a long history and an evolving specification. In this paper, we say “JavaScript” toroughly mean ECMAScript Edition 3, the standard versionof the language for more than a decade [24]. We say “ES5”to refer to Edition 5 of the language, recently released by the
JavaScript standards committee [13]; Edition 4 was neverstandardized. We say “ES6” to refer to features proposed forthe next version of the language, scheduled to be finalized
within the next one or two years. DJS includes a large set ofcore features common to all editions.
2.1

Base Types, Operators, and Control Flow

Consider the following function adapted from [9] and annotated in DJS. A function type annotation is written just above
the definition inside a JavaScript comment demarcated by anadditional : character. We typeset annotations in math modefor clarity, but the ASCII versions parsed by our type checker
are quite similar.

Let us begin with an informal overview of the semantics
of JavaScript. We will emphasize the aspects that are themost distinctive and challenging from the perspective of typesystem design, and describe the key insights in our work that
overcome these challenges.

/*: x ∶ Top → {ν ∣ ite Num(x) Num(ν) Bool (ν)} */function negate(x) {if (typeof x == "number") { return 0 - x; }else
{ return !x;} }JavaScript Semantics by Desugaring. Many corner casesof JavaScript are clarified by λJS [21], a syntax-directedtranslation, or desugaring, of JavaScript programs to amostly-standard lambda-calculus with explicit references.

The typeof operator is a facility used pervasively to directcontrol flow based on the run-time “tag” of a value. If the
input to negate is a number, so is the return value. If not, thefunction uses an interesting feature of JavaScript, namely,val typeof :: (* x ∶ Top → {ν = tag(x)} *)val! :: (* x ∶ Top → {ν iff falsy(x)} *)val(||) :: (* x ∶ Top → y ∶ Top → {ite falsy(x) (ν = y) (ν = x)} *)val(&&) :: (* x ∶ Top → y ∶ Top → {ite truthy(x) (ν = y) (ν = x)} *)val (===) :: (* x ∶ Top → y ∶ {tag(ν) = tag(x)} → {ν iff (x = y ∧ x ≠ NaN)} *)val(==) :: (* x ∶ Top → y ∶ Top → {Bool (ν) ∧ (tag(x) = tag(y) ⇒ ν iff (x = y ∧ x ≠ NaN))} *)val(+) :: (* x ∶ Str → y ∶ Str → Str *)val(+) :: (* x ∶ Num → y ∶ Num → {Num(ν) ∧ ((Int(x) ∧ Int(y)) ⇒ (Int(ν) ∧ ν = x + y))} *)val
fix :: (* ∀A. (A → A) → A *)Figure 2. Excerpt from basics.drefthat all values have a boolean interpretation. The values
false, null, undefined, the empty string “”, 0, and the“not-a-number” value NaN are considered falsy, and evaluate
to false when used in a boolean context; all other values aretruthy. The operator ! inverts “truthiness,” so the else branch
returns a boolean no matter what the type of x is. The ability
to treat arbitrary values as booleans is commonly used, forexample, to guard against null values.
The negate function demonstrates that even simple
JavaScript programs depend heavily on sophisticated controlflow based reasoning. Syntactic type systems are capable oftracking control flow to a limited degree [22, 36], but none
can handle complex invariants like the relationship between
the input and output of negate. To have any chance of capturing such invariants, types must be able to depend on otherprogram values. Powerful dependent type systems like Coq
can express extremely rich invariants, but are too heavyweight for our goals since they require the programmer todischarge type checking obligations interactively.
Refinement Types. We adopt a more lightweight mechanism called refinement types that has been previously applied to purely functional dynamic languages [5, 9]. We
demonstrate that refinement types afford us the expressiveness needed to precisely track control-flow invariants in the
JavaScript setting and, unlike more powerful dependent systems, without sacrificing decidable type checking. In particular, once the programmer has written type annotations forfunction definitions, type checking is carried out automatically via a combination of syntactic subtyping and SMTbased [11] logical validity checking.
In System !D, every value is described by a refinement
type of the form {ν ∣ p}, read “ν such that p”, where p
is a formula that can mention ν. For example, 3 can begiven the type {ν ∣ tag(ν) = “number”} and true the type{ν ∣ tag(ν) = “boolean”}, where tag is an uninterpretedfunction symbol in the refinement logic, not a function in the
programming language. We define abbreviations in Figure 3
to make the refinement binder implicit and the types concise.
Primitives. We use refinements to assign precise, andsometimes exact, types to System !D primitive functions,○○{p} = {ν ∣ p} Num(x) = tag(x) = “number”○○
Top(x) = true
Bool (x) = tag(x) = “boolean”○○
T = {T (ν)} Str (x) = tag(x) = “string”○○

if p then q1 else q2 = ite p q1 q2 = (p ⇒ q1 ) ∧ (¬p ⇒ q2 )○x iff p = ite p (x = true) (x = false)○

falsy(x) = x ∈ {false ∨ null ∨ undefined ∨ “” ∨ 0 ∨ NaN}○
truthy(x) = ¬falsy(x)Figure 3. Abbreviations for common types
defined in the file basics.dref (Figure 2). Notice thattypeof returns the tag of its input. Some examples beyond
ones we have already seen include tag(null) = “object”
and tag(undefined) = “undefined”. The type of thenegation operator ! inverts “truthiness.” The types of the operators && and || are interesting, because as in JavaScript,
they do not necessarily return booleans. The “guard” operator && returns its second operand if the first is truthy, whichenables the idiom if (x && x.f) { ... } that checks
whether the object x and its “f” field are non-null. Dually,
the “default” operator || returns its second operand if thefirst is falsy, which enables the idiom x = x || default
to specify a default value. The + operator is specified as anintersection of function types and captures the fact that it
performs both string concatenation and numerical addition,
but does not type check expressions like 3 + “hi” that relyon the implicit coercion in JavaScript. We choose types for
System !D primitives that prohibit implicit coercions since
they often lead to subtle programming errors.
Equality. JavaScript provides two equality operators: ==implicitly coerces the second operand if its tag differs fromthe first, and strict equality === does not perform any coercion. To avoid reasoning about implicit coercions, we give a
relatively weaker type to ==, where the boolean result relates
its operands only if they have the same tag.
Integers. JavaScript provides a single number type that has
no minimum or maximum value. However, programmers
and optimizing JIT compilers [38] often distinguish integers
from arbitrary numbers. In System !D, we describe integers○
with the abbreviation Int(x) = Num(x) ∧ integer (x). We
introduce the uninterpreted predicate integer (x) in the types

function also_negate(x) {if (typeof x == "number")x = 0 - x;
else
x = !x;

return x;}

let also_negate = fun x ->(* Γ1 = ∅; Σ1 = ∅ *)let _x = ref x in(* Γ2 = x ∶ Top; Σ2 = (`x ↦ x) *)if typeof (deref _x) == "number" then(* Γ3 = Γ2 , x ∶ Ref `x ; Σ3 = Σ2 *)_x := 0 - (deref _x)(* Γ4 = Γ3 , Num(x); Σ4 = ∃x4 ∶ Num. (`x ↦ x4 ) *)else
_x := !(deref _x) (* Γ6 = Γ3 , ¬Num(x); Σ6 = ∃x6 ∶ {ν iff falsy(x)}. (`x ↦ x6 ) *);(* Γ7 = Γ3 ; Σ7 = ∃x′ ∶ {ite Num(x) Num(ν) Bool (ν)}. (`x ↦ x′ ) *)deref _x in(* Γ8 = Γ3 ; Σ8 = Σ7 *)let _also_negate = ref {"__code__": also_negate}

Figure 4. DJS function also negate; Desugared to System !D; Verifying x∶Top → {ite Num(x) Num(ν) Bool (ν)}
of integer literals, and functions like + propagate “integerness” where possible. Furthermore, numeric functions use
the (decidable) theory of linear arithmetic to precisely reason
about integers, which is important for dealing with arrays.

follow the λJS encoding for simplicity. For System !D toverify that also_negate satisfies the specification, it must
precisely reason about heap updates in addition to controlflow as before.

Tracking Control Flow. System !D tracks control flow
precisely by recording that the guard of an if-expression istruthy (resp. falsy) along the then-branch (resp. else-branch),enabling System !D to verify the annotation for negate as
follows. Because of the call to typeof, System !D tracks
that Num(x) holds along the then-branch, so x can be safely
passed to the subtraction operator which produces a number
as required. For the else-branch, System !D records that
¬Num(x). The negation operator, which can be applied
to any value, produces a value of type {ν iff ¬falsy(x)}which is a subtype of Bool . Thus, both branches satisfy the
specification provided by the programmer.

Reference Types. The traditional way to handle referencesin the λ-calculus [28] is to (a) assign a reference cell some
type Ref T , (b) require that only values of type T be stored init, and then (c) conclude that dereferences produce values oftype T . This approach supports so-called weak updates, because even if a stored value satisfies a stronger type S than
T (i.e., if S is a subtype of T ), subsequent dereferences produce values of the original, weaker type T . Put another way,
this approach requires that the type assigned to a referencecell be a supertype of all the values written to the cell. Unfortunately, weak updates would preclude System !D fromverifying also_negate. The initialization of _x on line 2
stores the parameter x which has type Top, so _x would be
assigned type Ref Top. The assignments on lines 4 and 6
type check because the updated values satisfy the trivial typeTop, but the dereference on line 8 produces a value with typeTop, which does not satisfy the specified return type. Thus,
we need a way to reason more precisely about heap updates.

2.2

Imperative Updates

JavaScript is an imperative language where variables canbe reassigned arbitrary values. Consider the DJS function
also_negate in Figure 4 that is like negate but first assigns the eventual result in the variable x, and its translation
to System !D on the right (ignore the comments for now).
Several aspects of the translation warrant attention. First,
since the formal parameter x, like all JavaScript variables,
is mutable, the translation of the function body begins withan explicit reference cell _x initialized with x, and each readof x is desugared to a dereference of _x. Presentations ofimperative languages often model assignable variables directly rather than with explicit references. Both approaches
are equivalent; we choose the latter to make the presentation more similar to λJS [21] and System D [9]. Second,
notice that scalar constants like 0 and true and operators
like typeof and == are translated directly to corresponding
ones in System !D. Third, notice that each assignment to thevariable x translates to a set reference (i.e., assignment) operation to update the contents of the heap cell. Finally, since
every JavaScript function is actually an object, the translation stores the function value in a distinguished “ code ”
field, which we assume is inaccessible to source programs.
Instead of this assumption, we could treat each function asa pair of a function value and an associated object, but weStrong Updates. Allowing assignment to change the typeof a reference is called strong update, which is sound only
when a reference is guaranteed to point to a single heap celland when there are no accesses through other aliases that refer to the same cell. The Alias Types approach [32] provides
a means of managing these concerns. Rather than Ref T , areference type is written Ref `, where ` is the (compile-time)
name of a location in the heap, and a separate (compiletime) heap maps locations to types, for example, (` ↦ T ).
Strong updates are realized by allowing heaps to change
flow-sensitively, and the aliasing problem is mitigated bymaintaining the invariant that distinct location names ` and`′ do not alias. System !D employs this approach by using atype environment Γ that grows and shrinks as usual during
type checking but remains flow-insensitive, and a heap environment Σ that can be strongly updated per program point.
Figure 4 shows how System !D checks the desugared
version of also_negate. The figure shows, at each line i,
the type environment Γi used to check the expression on theline, and the heap environment Σi that exists after checking

the expression. After starting with the empty heap Σ1 = ∅,the allocation on line 2 creates a fresh location `x in the new○heap Σ2 = Σ1 ⊕ (`x ↦ x) and adds x∶Ref `x to the typeenvironment. We use the symbol ⊕ to construct unorderedsets of heap bindings. To exploit the precision of dependent
types, we map locations to values rather than types (i.e.,(` ↦ x) rather than (` ↦ Top)).
When checking the if-expression guard on line 3, thedeference retrieves the initial value x from the heap Σ2 , so as
a result of the tag-test, System !D adds Num(x) to the typeenvironment Γ4 along the true-branch and ¬Num(x) to Γ6along the false-branch. In the true-branch, the subtraction
on line 4 is well-typed because Num(x), and produces a
number x4 that is stored in the heap Σ4 at location `x . In
the false-branch, x is negated on line 6, producing a boolean
x6 that is stored in the heap Σ6 at location `x . System !D
combines the branches by joining the heaps Σ4 and Σ6 ,producing Σ7 that describes the heap no matter which branchis taken. The dereference on line 8 retrieves x′ , a value oftype {ite Num(x) Num(ν) Bool (ν)}, as required by the
return type annotation.
In this way, System !D syntactically tracks strong updates
to the heap, while reducing subtyping obligations to implication queries in an ordinary, pure refinement logic [9] that
does not model imperative updates.
2.3

trieves the key k from dictionary d, where sel (d, k) describes the exact binding as a value in the refinement logic;
set d k y produces a new dictionary that extends d with abinding for k, shadowing previous bindings, if any, whereupd (d, k, y) describes the new dictionary; del d k produces a new dictionary with a binding removed, using the
logical symbol bot (distinct from all source-level values)
to denote its absence; and mem d k indicates the presenceor absence of a binding, where we write the abbreviation○has(d, k) = sel (d, k) ≠ bot.
The key innovation of nested refinements in System D
allows syntactic type terms U (like function types) to be
written within refinement formulas using an uninterpreted“has-type” predicate x ∶∶ U , while staying within the decidable McCarthy theory of arrays [27]. The has-type predicate allows System D to describe dictionaries that map
dynamic keys to arbitrary values. For example, we write{Dict(ν) ∧ sel (ν, k) ∶∶ Bool → Bool } to describe a dictionary d with key k that binds a boolean-to-boolean function,and {ν = upd (d, “g”, 4)} to describe a dictionary d′ that isjust like d but with an additional binding. Prior approaches
such as [5] were limited to dynamic keys that store first-order(non-function) values. We refer the reader to [9] for the technical development of nested refinements.
Mutability and Dynamic Keys. The combination of nested
refinements and strong updates allows us to precisely track
objects with dynamic keys despite the presence of imperative updates. Consider the desugaring of our example above;
we omit the assertions for clarity.

Simple Objects

JavaScript’s objects exhibit several interesting semantic
properties. Consider the following object initialized witha single key (also known as field or property). We assume
that assert is a pre-defined function that aborts when its argument is falsy; JavaScript does not provide such a function
as built-in, but it is trivial to define.
var x = {"f": 1};
assert (x.f == 1 && x.g == undefined);x.g = 2; delete x.f;
assert (x.g == 2 && x.f == undefined);
x.f.g; // raises exception
var k = "h"; x[k] = 3; assert (x[k] == 3);

Notice that when retrieving the non-existent “g” key fromx, JavaScript returns undefined as opposed to raising an
exception. Attempting to retrieve a key from undefined,or null, however, does raise an exception. Keys can be
added or removed to objects, and can even be arbitrary
dynamically-computed values, not just string literals, that areconverted to strings if necessary. Dynamic keys are pervasive— objects are commonly used as hash tables with unknown
sets of keys — but they are quite challenging to track inside
a static type system.
Nested Refinements. To support dynamic keys, we adopt
the System D primitives [9] for (functional) dictionary operations, shown in the first four lines of the file objects.dref(Figure 5). The primitive function application get d k re-








let _x = ref (ref {"f": 1}) in_x := set (deref (deref _x)) "g" 2;_x := del (deref (deref _x)) "f";let _k = "h" in_x := set (deref (deref _x))
(coerceToStr (deref _k)) 3;

The allocation on line 1 adds three bindings to the typeenvironment — d∶{ν = upd (empty, “f”, 1)}, ptr ∶Ref `,and obj∶Ref `′ , where ` and `′ are fresh locations —○and produces the heap Σ1 = (`′ ↦ ptr ) ⊕ (` ↦ d). Notice that the dictionary is stored via an additional levelof indirection to facilitate the encoding of side-effecting
JavaScript object operations. The object extension on line
2 adds d′ ∶{ν = upd (d, “g”, 2)} to the type environment and○strongly updates the heap to Σ2 = (`′ ↦ ptr ) ⊕ (` ↦ d′ ).
The deletion on line 3 and the extension on line 5 (through adynamic key) have similar effects on the static heap, thereby
statically verifying the assertions.
2.4

Function Types

In order to fully understand the challenges of JavaScript
objects, we must pause to take a closer look at function
types. The function types we have seen so far — for negate
and the primitives in basics.dref — have not mentioned

val
val
val
val

set :: (* d ∶ Dict → k ∶ Str → y ∶ Top → {ν = upd (d, k, y)} *)del :: (* d ∶ Dict → k ∶ Str → {ν = upd (d, k, bot)} *)has :: (* d ∶ Dict → k ∶ Str → {ν iff has(d, k)} *)get :: (* d ∶ Dict → k ∶ Str → {ite has(d, k) (ν = sel (d, k)) (ν = undefined)} *)val setPropObj :: (* (x ∶ Ref , k ∶ Str , y ∶ Top)/(x ↦ ⟨d ∶ Dict, ẋ⟩) → {ν = y}/(x ↦ ⟨d′ ∶ {ν = upd (d, k, y)}, ẋ⟩) *)val delPropObj :: (* (x ∶ Ref , k ∶ Str )/(x ↦ ⟨d ∶ Dict, ẋ⟩) → Bool /(x ↦ ⟨d′ ∶ {ν = upd (d, k, bot)}, ẋ⟩) *)val hasPropObj :: (* (x ∶ Ref , k ∶ Str )/(x ↦ ⟨d ∶ Dict, ẋ⟩) → {ν iff ObjHas(d, k, cur , ẋ)}/same *)val getPropObj :: (* (x ∶ Ref , k ∶ Str )/(x ↦ ⟨d ∶ Dict, ẋ⟩)→ {ite ObjHas(d, k, cur , ẋ) (ν = ObjSel (d, k, cur , ẋ)) (ν = undefined)}/same *)getIdxArr :: (* ∀A. (x ∶ Ref , i ∶ Int)/(x ↦ ⟨a ∶ Arr (A), ẋ⟩)→ {ite ¬packed (a) (ν ∶∶ A ∨ Undef (ν)) (ite (0 ≤ i < len(a)) (ν ∶∶ A) (Undef (ν)))}/same *)val getLenArr :: (* ∀A. (x ∶ Ref , k ∶ {ν = “length”})/(x ↦ ⟨a ∶ Arr (A), ẋ⟩)→ {ite packed (a) (ν = len(a)) Int(ν)}/same *)val getPropArr :: (* ∀A. (x ∶ Ref , k ∶ {Str (ν) ∧ ν ≠ “length”})/(x ↦ ⟨a ∶ Arr (A), ẋ⟩)→ {ite HeapHas(H, ẋ, k) (ν = HeapSel (H, ẋ, k)) (ν = undefined)}/same *)
val

val
val

getElem :: (and (type getPropObj) (type getIdxArr) (type getLenArr) (type getPropArr))
setIdxArr :: (* ∀A. (x ∶ Ref , i ∶ Int, y ∶ A)/(x ↦ ⟨a ∶ Arr (A), ẋ⟩)
→ {ν = y}/(x ↦ ⟨a′ ∶ {ν ∶∶ Arr (A) ∧ arrSet(ν, a, i)}, ẋ⟩) *)Figure 5. Excerpt from objects.dref
heaps, because their inputs and outputs are scalar values.
However, JavaScript objects are reference values, and arepassed to and returned from functions through the heap.
Thus, to account for heaps and side-effects, a System !Dfunction type has the following form.

heap, where each binding records that the final value isexactly equal to the initial value.
• In an input world, a reference binding x∶Ref without alocation introduces a location variable L that is quantified
by the type, and x (a value of type Ref L) can be used asa location in heaps to refer to this variable L. Further,
the dotted variable ẋ introduces a location parameter,
corresponding to the prototype of x.

∀[A; L; H] x1 ∶ T1 / Σ̂1 → x2 ∶ T2 / Σ̂2This type describes a function that, given an argument x1 oftype T1 in a calling context that satisfies the input heap typeΣ̂1 , produces an output value x2 of type T2 and a modified
heap type Σ̂2 . A function type can be parameterized by sequences of type variables A, location variables L, and heap
variables H. A heap type Σ̂ is like a heap environment Σ butmaps locations to binder-type pairs rather than values (e.g.,(` ↦ y ∶T ) rather than (` ↦ v)); the binders name the values
stored in the heap before and after a function call. The binder
x1 and all of the binders in the input heap Σ̂1 are in scopein the output world x2 ∶T2 / Σ̂2 . Intuitively, a world describes
a tuple where every component except the first resides in aheap. We often omit binders when they are not referred to. To
match the structure of function types, function applications
must instantiate type, location, and heap variables. However,
our implementation infers instantiations in almost all cases
using standard local type inference techniques (§ 6). Whenwe write DJS examples in the sequel, we omit instantiations
at applications wherever our current implementation infers
them. We sweeten function type syntax with some sugar:• When used as an output heap, the token same refers

to the sequence of locations in the corresponding input• A heap variable H is implicitly added to a function typewhen it contains none, and H is added to both the input and output heaps; this variable corresponds to the“frame” from separation logic [17]. In this case, the token cur refers to H.
For example, compare the type for hasPropObj (Figure 5)
followed by its expansion.
(x ∶ Ref , k ∶ Str )/(x ↦ ⟨d ∶ Dict, ẋ⟩)
→ {ν iff ObjHas(d, k, cur , ẋ)}/same∀L, L′ , H. (x ∶ Ref L, k ∶ Str )/H ⊕ (L ↦ ⟨d ∶ Dict, L′ ⟩)→ {ν iff ObjHas(d, k, H, L′ )}/H ⊕ (L ↦ ⟨d′ ∶ {ν = d}, L′ ⟩)2.5

Prototype-Based Objects

JavaScript sports a special form of inheritance, where eachbase object is equipped with a link to its prototype object.
This link is set when the base object is created and cannot bechanged or accessed by the program. When trying to retrievea key k not stored in an object x itself, JavaScript transitively
searches the prototype chain of x until it either finds k or itreaches the root of the object hierarchy without finding k.

The prototype chain does not play a role in the semantics of
key update, addition, or deletion.1
For example, consider the initially empty object childcreated by the function beget (described in the sequel) with
prototype object parent. The prototype of object literals,
like parent, is the object stored in Object.prototype(note that the “prototype” key of Object is not thesame as its prototype object). Thus, all keys in parent andObject.prototype are transitively accessible via child.
var parent = {"last": " Doe"};var child = beget(parent);child.first = "John";assert (child.first + child.last == "John Doe");assert ("last" in child == true);assert (child.hasOwnProperty("last") == false);

The JavaScript operator k in x tests for the presence of k
anywhere along the prototype chain of x, whereas the native
function Object.prototype.hasOwnProperty tests only
the “own” object itself. Keys routinely resolve through prototypes, so a static type system must precisely track them.
Unfortunately, we cannot encode prototypes directly within
the framework of refinement types and strong update, as thesemantics of transitively traversing mutable and unbounded
prototype hierarchies is beyond the reach of decidable, firstorder reasoning.
Shallow and Deep Heaps. We solve this problem by syntactically reducing reasoning about prototype-based objects
to the refinement logic. Our key insight is to decompose
the heap into a “shallow” part, the bounded portion of theheap for which we have explicit locations, and a “deep” part,which is the potentially unbounded portion which we canrepresent by uninterpreted heap variables H. We explicitly
track prototype links in the “shallow” heap by using bindings of the form (` ↦ ⟨d, `′ ⟩), where the prototype of theobject at ` is stored at `′ . We cannot track prototype links
explicitly in the “deep” heap, so instead we summarize information about deep prototype chains by using the abstract(uninterpreted) heap predicate HeapHas(H, `, k) to encode
the proposition that the object stored at location ` in H transitively has the key k, and the abstract (uninterpreted) heap
function HeapSel (H, `, k) to represent the corresponding
value retrieved by lookup.
As an example, recall the child object and its prototype
parent. Suppose that the prototype of parent is an unknown object grandpa, rather than Object.prototype
as written. If child, parent, and grandpa are stored
at locations `1 , `2 , and `3 with underlying “own” dictionary values d1 , d2 , and d3 , then we write the heap{`1 ↦ ⟨d1 , `2 ⟩, `2 ↦ ⟨d2 , `3 ⟩, `3 ↦ ⟨d3 , `4 ⟩, H} — we use
set notation to abbreviate the concatenation of heap bindings
1 Many implementations expose the prototype of an object x with a non-standard x. proto property, and prototypes do affect key update in ES5.
We discuss these issues further in §7.

with ⊕. Despite not knowing what value is the prototype of
grandpa, we name its location `4 that is somewhere in the
deep part of the heap H.
Key Membership and Lookup. When describing simple
objects, we used the original System D primitives (mem andget) to desugar key membership and lookup operations. But
in fact, to account for the transitive semantics of key membership and lookup facilitated by prototype links, System !Duses new primitives hasPropObj and getPropObj definedin objects.dref (Figure 5). These primitives differ fromtheir purely functional System D counterparts in two ways:
each operation goes through a reference to a dictionary on
the heap, and the abstract predicates ObjHas and ObjSel
are used in place of has and sel . These abstract predicatesare defined over the disjoint union of the shallow and deep
heaps as follows and, intuitively, summarize whether an object transitively has a key and, if so, the value it binds.
○

ObjHas(d, k, H, ẋ) = has(d, k) ∨ HeapHas(H, ẋ, k)○ν = ObjSel (d, k, H, ẋ) = if has(d, k) then ν = sel (d, k)else ν = HeapSel (H, ẋ, k)Transitive Semantics via Unrolling. Let us return to theexample of the child, parent and grandpa prototype
chain to understand how unrolling captures the semantics
of transitive lookup. The DJS key membership test on theleft desugars to System !D on the right as follows.
k in child

hasPropObj (deref _child, deref _k)

The result of the function call has the following type.
{ν iff ObjHas(d1 , k, {(`2 ↦ ⟨d2 , `3 ⟩), (`3 ↦ ⟨d3 , `4 ⟩), H}, `2 )}We expand this type by unrolling ObjHas to the following.
{ν iff has(d1 , k) ∨ has(d2 , k) ∨ has(d3 , k) ∨ HeapHas(H, `4 , k)}

The first three disjuncts correspond to looking for k in theshallow heap, and the last is the uninterpreted predicate thatsummarizes whether k exists in the deep heap. Similarly, key
lookup in DJS on the left is desugared as follows.
child[k]getPropObj (deref _child, deref _k)

We unroll the type of the System !D expression as follows.
{if has(d1 , k) then ν = sel (d1 , k) else
if has(d2 , k) then ν = sel (d2 , k) else
if has(d3 , k) then ν = sel (d3 , k) else
ite HeapHas(H, `4 , k) (ν = HeapSel (H, `4 , k)) Undef (ν)}

Thus, our technique of decomposing the heap into shallow
and deep parts, followed by heap unrolling, captures the exact semantics of prototype-based object operations modulo
the unknown portion of the heap. Thus, System !D precisely
tracks objects in the presence of mutation and prototypes.

var __hasOwn =˙/*: (this ∶ Ref , k ∶ Str )/(this ↦ ⟨d ∶ Dict, this⟩)→ {ν iff has(d, k)}/same˙∧ ∀A. (this ∶ Ref , i ∶ Int)/(this ↦ ⟨a ∶ Arr (A), this⟩)→ {ite packed (a) (ν iff 0 ≤ i < len(a)) Bool (ν)}/same˙∧ ∀A. (this ∶ Ref , k ∶ Str )/(this ↦ ⟨a ∶ Arr (A), this⟩)→ {ν iff k = “length”}/same */ "#extern";function Object() { ... }; Object.prototype = {"hasOwnProperty": __hasOwn, "constructor": Object, ... };˙
var __push = /*: ∀A. (this ∶ Ref , x ∶ A)/(this ↦ ⟨a ∶ Arr (A), this⟩)˙→ Int /(this ↦ ⟨a′ ∶ {ν ∶∶ Arr (A) ∧ arrSize(ν, a, 1)}, this⟩)*/ "#extern";˙
var __pop = /*: ∀A. (this ∶ Ref , x ∶ A)/(this ↦ ⟨a ∶ Arr (A), this⟩)→ {ite packed (a) (ν ∶∶ A) (ν ∶∶ A ∨ Undef (ν))}˙/ (this ↦ ⟨a′ ∶ {ν ∶∶ Arr (A) ∧ arrSize(ν, a, −1)}, this⟩)*/ "#extern";function Array() { ... }; Array.prototype = {"push": __push, "pop": __pop, "constructor": Array, ... };Figure 6. Excerpt from prelude.js, which desugars to the prelude.dref file in the standard prelude
Additional Primitives. The new update and deletion primitives setPropObj and delPropObj (Figure 5) affect only
the “own” object, since the prototype chain does not participate in the semantics. We model native JavaScript functions
like Object.prototype.hasOwnProperty with type annotations in the file prelude.js (Figure 6). Notice that thefunction type for objects (the first in the intersection) checks
only the “own” object for the given key.
Constructors. JavaScript provides the expression form
new Foo(args) as a second way of constructing objects,
in addition to object literals whose prototypes are set to
Object.prototype. The semantics are straightforward,
but quite different than the traditional new syntax suggests.
Here, if Foo is any function (object), then a fresh, empty object is created with prototype object Foo.prototype, andFoo is called with the new object bound to this (alongwith the remaining arguments) to finish its initialization.
We desugar constructors and new with standard objects andfunctions (following λJS [21]) without adding any special
System !D constructs or primitive functions.
Inheritance. Several inheritance relationships, includingones that simulate traditional classes, can be encoded withthe construction mechanism, as shown in the popular book
JavaScript: The Good Parts [10]. Here, we examine the prototypal pattern, a minimal abstraction which wraps construction to avoid the unusual syntax and semantics that leads
to common errors; we discuss the rest in § 6. The function
beget (the basis for Object.create in ES5) returns a fresh
empty object with prototype o.








/*: ∀L. o ∶ Ref /(o ↦ ⟨d ∶ Dict, ȯ⟩)→ Ref L/(L ↦ ⟨{ν = empty}, o⟩) ⊕ (o ↦ same) */function beget(o) {/*: #ctor this ∶ Ref → {ν = this} */function F() { return this; };F.prototype = o;return new /*:L*/ F();}

The #ctor on line 4 instructs desugaring to: initialize thefunction object with a “prototype” key that stores anempty object literal (since it will be called as a constructor);and expand the type annotation as follows to require that
this initially be empty, as is common for all constructors.
˙
this ∶ Ref /(this ↦ ⟨{ν = empty}, this⟩)→ {ν = this}/same

The assignment on line 6 strongly updates Foo.prototype(overwriting its initial empty object) with the argument o.
Thus, the object constructed (at location L) on line 7 has
prototype o, so beget has the ascribed type. In most cases,
new can be used without a location annotation and a fresh
one is chosen. In this case, we annotate line 7 with L (fromthe type of beget), which our implementation does not inferbecause there is no input corresponding to L.
2.6

ArraysThe other workhorse data structure of JavaScript is the array, which is really just an object with integer “indices” converted to ordinary string keys. However, arrays pose several
tricky challenges as they are commonly used both as finite
tuples as well as unbounded collections.
var arr = [17, "hi", true];arr[3] = 3; arr.push(4);assert (arr.length == 5 && arr[5] == undefined);

As for any object, retrieving a non-existent key returns
undefined rather than raising an “out-of-bounds” exception. Like other objects, arrays are extensible simply by
writing “past the end.” Array literal objects have prototype Array.prototype, which includes a push (resp. pop)function for adding an element to (resp. removing an element from) the end of an array.
Loops are used to iterate over arrays of unknown size. But
since lookups may return undefined, it is important to track
when an access is “in-bounds.” JavaScript bestows uponarrays an unusual “length” property, rather than a method,

(A1) a contains the special “length” key.

Array Primitives. We define several array-manipulating
primitives in objects.dref (some of which we show
in Figure 5) that maintain and use the array invariants
above. For key lookup on arrays, we define three primitives: getIdxArr looks for the integer key i on the own
object a and ignores the prototype chain of a because (A4)guarantees that a will not inherit i, and returns a value subject to the properties (A3) and (A5) that govern its integer
key bindings; getLenArr handles the special case when thestring key k is “length”, which (A1) guarantees is boundby a, and returns the the true length of the array only if it ispacked; and getPropArr deals with all other (safe) string
keys k by reading from the prototype chain of the array(re-using the heap unrolling mechanism) ignoring its own
bindings because of (A2).
For array updates, we define setIdxArr that uses the following macros to preserve packedness (A5) when possible.

(A2) All other “own” keys of a are (strings that coerce to)integers.

arrSet(a′ , a, i) = if 0 ≤ i < len(a) then arrSize(a′ , a, 0) else
if i = len(a) then arrSize(a′ , a, 1) else true(A3) For all integers i, either a maps the key i to a value oftype T , or it has no binding for i.

arrSize(a′ , a, n) = packed (a) ⇒(packed (a′ ) ∧ len(a′ ) = len(a) + n)

to help. Reading it returns the largest integer key of the array,
which is not necessarily its “size” because it may contain“holes” or even non-integer keys. Furthermore, assigning a
number n to the “length” of an array either truncates it if
n is less than its current length, or extends it (by padding
with holes) if it is greater. Despite the unusual semantics,
programmers commonly use arrays as if they are traditional“packed” arrays with integer “indices” zero to “size” minus
one. The type system must reconcile this discrepancy.
Array Types. We introduce a new syntactic type term
Arr (T ) and maintain the following four properties for every value a that satisfies the has-type predicate a ∶∶ Arr (T ).
We refer to strings that do not coerce to integers as “safe,”
and we use an uninterpreted predicate safe to describe suchstrings (e.g., safe(“foo”) whereas ¬safe(“17”)).

(A4) All inherited keys of a are safe (i.e., non-integer) strings.
An array can have arbitrary objects in its prototype chain,so to ensure (A4), we require that all non-array objects bind
only safe strings. This sharp distinction between between array objects (that bind integer keys) and non-array objects(that bind safe string keys) allows System !D to avoid reasoning about string coercions, and does not significantly
limit expressiveness because, in our experience, programs
typically conform to this division anyway. To enforce thisrestriction, the type for keys manipulated by primitives inobjects.dref and prelude.js is actually SafeStr , rather○
than Str as shown in Figure 5 and Figure 6, where SafeStr ={Str (ν) ∧ safe(ν)}. We discuss an alternative approach in§7 that allows non-array objects to bind unsafe strings.
Packed Arrays. Arrays a that additionally satisfy the uninterpreted predicate packed (a) enjoy the following property,
where len(a) is an uninterpreted function symbol.
(A5) For all integers i, if i is between zero and len(a) minus
one, then a maps i to a value of type T . Otherwise, a has
no binding for i.
Tuple Arrays. Using additional predicates, System !Dgives precise types to array literals, which are often usedas finite tuples in idiomatic code. For example, we can describe pairs as follows:○(Int, Int) = {ν ∶∶ Arr (Int) ∧ packed (ν) ∧ len(ν) = 2}○

(Bool , Str ) = {ν ∶∶ Arr (Top) ∧ packed (ν) ∧ len(ν) = 2∧ Str (sel (ν, 0)) ∧ Bool (sel (ν, 1))}Thus, the technique of nested refinements allows us tosmoothly reason about arrays both as packed homogeneouscollections as well as heterogeneous tuples.

○○

In particular, the updated array a′ is packed if: (1) the original array a is packed; and (2) the updated index i is either
within the bounds of a (in which case, the length of a′ is thesame as a) or just past the end (so the length of a′ is one
greater than a). In similar fashion, we specify the remaining
primitives for update and deletion to maintain the array invariants, and the ones for key membership to use them, but
we do not show them in Figure 5.
In prelude.js (Figure 6), we use precise types to model
the native push and pop methods of Array.prototype(which maintain packedness, as above), as well as the behavior of Object.prototype.hasOwnProperty on arrays(the last two cases of the intersection type). Thus, the precise dependent types we ascribe to array-manipulating operations maintain invariants (A1) through (A5) and allow DJS
to precisely track array operations.
Desugaring. It may seem that we need to use separate
primitive functions for array and non-array object operations, even though they are syntactically indistinguishable in
JavaScript. Nevertheless, we are able to desugar DJS based
purely on expression syntax (and not type information) byunifying key lookup within a single primitive getElem andgiving it a type that is the intersection of the (three) array
lookup primitives and the (one) non-array lookup primitive
getPropObj. We define getElem in Figure 5, where we
specify the intersection type using and and type as syntactic sugar to refer to the previous type annotations. We define similar unified primitives for setElem, hasElem, anddelElem (not shown in Figure 5). Desugaring uniformly
translates object operations to these unified general primitives, and type checking of function calls ensures that theappropriate cases of the intersection type apply.

2.7

Collections

As discussed in §2.2, strong updates are sound only for references that point to exactly one object, which is far too restrictive as real programs manipulate collections of objects.
In this section, we describe weak references in DJS to refer
to multiple objects, a facility that enables programming witharrays of mutable objects as well as recursive types.
Weak References. In the following example, we iterateover an array of passenger objects and compute the sumof their weights; we use a default value max_weight whena passenger does not list his weight (ignore the unfamiliar
annotations for now).









/*: (`˜pass ↦ frzn) → same */for (i=0; i < passengers.length; i++) {var p = passengers[i];/*: #thaw p */if (p.weight) { sum += p.weight;}
else{ sum += max_weight; }/*: #freeze p */}We could describe the array passengers with the type Ref `for a location `. However, this type is not very useful as it
denotes an array of references to a single object.

to strongly update the type of the cell. While a location isthawed, the type system prohibits the use of weak references
to the location, and does not allow further thaw operations.
When the thawed (strong) reference is no longer needed, thetype system checks that the original type has been restored,
re-freezes the location, and discards the thawed location.
Soundness of the approach depends on the invariant thateach weak location has at most one corresponding thawed
location at a time.
In our example, we do not need to temporarily violate
the type of p, but the thaw/freeze mechanism does help
us relate the two accesses to p. The thaw state annotation
above the loop declares that before each iteration of the loop(including the first one), the location `˜pass must be frozen.
The thaw annotation on line 4 changes the type of p to astrong reference to a fresh thawed location `1 , which storesa particular dictionary on the heap (named with a binder)that is retrieved by both subsequent uses of p. Thus, we canrelate the key membership test to the lookup, and track thatp.weight produces a number. The freeze annotation on line
7 restores the invariant required before the next iteration. We
describe this technique further in §4.
Recursive Types. We reuse the weak location mechanism to describe recursive data structures. Consider thefollowing adapted from the SunSpider [34] benchmark
access-binary-trees.js, annotated in DJS.

Weak Locations. To refer to an arbitrary number (zeroor more) objects of the same type, we adopt the Alias
Types [32] solution, which categorizes some locations as
 /*: #define Ttn {“i” ∶ Num, “l”, “r” ∶ Ref `˜tn } */weak to describe an arbitrary number of locations that satisfy
 /*: #weak (`˜tn ↦ ⟨Ttn , `tnp ⟩) */the same type, and syntactically ensures that weak locations
 /*: #ctor (this ∶ Ref , left, right ∶ Ref `˜tn , item ∶ Num)
are weakly updated.
/(`˜tn ↦ frzn) → Ref `˜tn /same */We introduce a new kind of heap binding (`˜ ↦ ⟨T, `′ ⟩), function TreeNode(left, right, item) {where `˜ is a weak location, all objects that might reside there
this.l = left; this.r = right; this.i = item;/*: #freeze this */satisfy T , and `′ is the strong location of the prototype of all
˜ There is no heap binder for
return this;objects that reside at location `.
 }weak locations since there is not a single value to describe.
˜In our example, we can use (`˜pass ↦ ⟨Tpass , `op ⟩)  /*: this ∶ Ref `tn → Num */ TreeNode.prototype.itemCheck = function f() {to describe passenger objects, where `op is the location// thaw/freeze annotations inferredof Object.prototype and Tpass is the dictionary type if (this.l == null) return this.item;{Dict(ν)∧has(ν, “weight”) ⇒ Num(sel (ν, “weight”))}.
else { return this.i
˜
If we assign the type {ν ∶∶ Arr (Ref `pass ) ∧ packed (ν)}, + f.apply(this.l)to passengers, then p has type Ref `˜pass , and thus each - f.apply(this.r); }(desugared) use of p is a dictionary of type Tpass . This  }type is quite unsatisfying, however, because the conditional
establishes that along the then-branch, p does possess the
The source-level macro on line 1 introduces Ttn to abbrekey and therefore should be assigned the more precise typeviate the type of TreeNodes, using traditional record type
{Num(sel (d, “weight”))}.
syntax instead of the underlying McCarthy operators. Line
Thaw and Freeze. To solve this problem, we adopt a
2 defines the weak location for TreeNodes, using the premechanism found in derivatives of Alias Types (e.g., [2,dictable location `tnp created by desugaring for the object
12, 15, 31]) that allows a weak location to be temporarily
TreeNode.prototype. The constructor annotation itself
treated as strong. A weak location `˜ is said to be frozen if
declares that the return type is a reference to one of these
all references Ref `˜ use the location only at its weak (invarirecursive objects, which System !D verifies by checkingant) type. The type system can thaw a location, producing athat on line 6 the appropriate fields are added to the strong,strong reference Ref `k (with a fresh name) that can be used
initially-empty object this before it is frozen and returned.

Recursive Traversal. There are two differences in the
itemCheck function above compared to the original version, which cannot be type checked in DJS. First, we namethe function being defined (notice the f on line 11), a
JavaScript facility for recursive definitions. Second, we write
f.apply(this.r) instead of this.r.itemCheck() as in
the original, where the native JavaScript function apply allows a caller to explicitly supply a receiver argument. The
trouble with the original call is that it goes through the heap
(in particular, the prototype chain of this) to resolve the recursive function being defined. This function will be stored
in a strong object, and we have no facility (e.g., mu-types)
for strong objects with recursive types; our only mechanism
is for weak objects. If we write f.apply(this.r), however, the recursive function f is syntactically manifest, andwe can translate the definition with a call to the standard
fix primitive (Figure 2). In §5, we describe how we handle
a limited form of apply that is sufficient for our idiomaticrecursive definitions in DJS. We expect that we can add amore powerful mechanism for recursive types that supports
the original code as written, but we leave this to future work.
2.8

Rest of the Paper

We have now completed our tour of Dependent JavaScript.
Next, we formally define the syntax of System !D in § 3
and the type system in § 4. In, § 5, we present the syntax
of DJS and its desugaring to System !D. We discuss our
implementation and results in §6, directions for future workin § 7, and related work in § 8. Additional details may befound in an accompanying technical report [7].

3.

Syntax and Semantics of System !D

We now introduce the formal syntax of values, expressions,and types of System !D, defined in Figure 7.
Values. Values v include variables x, constants c, lambdas λx. e, (functional) dictionaries v1 ++ v2 ↦ v3 , andrun-time heap locations r. The set of constants c includes
base values (numbers, booleans, strings, the empty dictionary {}, null, undefined, NaN, etc.) and the primitive
functions from basics.dref and objects.dref (typeof,get, getElem, etc.). We use tuple syntax (v0 , . . ., vn ) as
sugar for the dictionary with fields “0” through “n” boundto the component values. Logical values w are all values andapplications of primitive function symbols F , such as addition + and dictionary selection sel , to logical values.
Expressions. We use an A-normal expression syntax sothat we need only define substitution of values (not arbitrary expressions) into types. We use a more general syntax
for examples throughout this paper, and our implementation
desugars expressions into A-normal form. Expressions e include values, function application, if-expressions, and letbindings. The ascription form e as T allows source-level
type annotations. Since function types will be parameterizedby type, location, and heap variables, the syntax of function
application requires that these be instantiated. Reference operations include reference allocation, dereference, and update, and the run-time semantics maintains a separate heapthat maps locations to values. The expression newobj ` v v ′stores the value v at a fresh location r — where the name` is a compile-time abstraction of a set of run-time location names that includes r – with its prototype link set tov ′ , which should be a location. The thaw ` v operation converts a weak reference to a strong strong one; freeze `˜ θ vconverts a strong reference to a weak one, where thaw stateθ is used by the type system for bookkeeping.
The operational semantics is standard, based on λJS withminor differences. For example, we make prototype links
manifest in the syntax of heaps (to facilitate heap unrollingin the type system), whereas λJS stores them inside objects
in a distinguished “ proto ” field. We refer the reader to[21] for the full details.
Types and Formulas. Values in System !D are describedby refinement types of the form {x ∣ p} where x may appear
free in the formula p and existential types ∃x∶T . S where x
may appear free in S. Rather than introduce additional syntactic categories, we assume, by convention, that existential
types do not appear in source programs; they are created only
during type checking in a controlled fashion that does notpreclude algorithmic type checking [25]. When the choiceof refinement binder does not matter, we write {p} as shorthand for {ν ∣ p}.
The language of refinement formulas includes predicatesP , such as equality and the dictionary predicate has, and theusual logical connectives. Similar to the syntax for expression tuples, we use (T1 , . . ., Tn ) as sugar for the dictionary type with fields “0” through “n” with the corresponding types. As in System D, we use an uninterpreted hastype predicate w ∶∶ U in formulas to describe values thathave complex types, represented by type terms U , which includes function types, type variables, null, reference, and array types. A reference type names a strong or weak locationin the heap, where a strong location ` is either a constant a
or a variable L and a weak location `˜ is a constant ã. We
discussed function types in § 2.4; now we use the metavariable W to range over worlds. A world x∶T / Σ̂ describes thebinders and types of a tuple of values, where every component except the first (x of type T ) resides in the heap Σ̂.
Heap Types. A heap type Σ̂ is an unordered set of heap
variables H and heap bindings ĥ concatenated with the⊕ operator. To simplify the presentation, we syntacticallyrequire that each heap has exactly one heap variable, so wewrite a heap type as the pair (H, ĥ), where H is the “deep”
part for which we have no information and ĥ is the “shallow”
part for which have precise location information. The heap
binding (` ↦ x∶T ) represents the fact that the value atlocation ` has type T ; the binder x refers to this value in thetypes of other heap bindings. The binding (` ↦ ⟨x∶T , `′ ⟩)Valuesv∶∶=

x ∣ c ∣ v1 ++ v2 ↦ v3 ∣ λx. e ∣ r

Expressions

e

∶∶=
∣

v ∣ [T ; `; Σ̂] v1 v2 ∣ if v then e1 else e2 ∣ let x = e1 in e2 ∣ e as T
ref ` v ∣ deref v ∣ v1 ∶= v2 ∣ newobj ` v v ′ ∣ freeze `˜ θ v ∣ thaw ` v

Types

S, T

∶∶=

{x ∣ p} ∣ ∃x ∶ T . S

Formulas

p, q

∶∶=

P (w) ∣ w ∶∶ U ∣ HeapHas(H, `, w) ∣ p ∧ q ∣ p ∨ q ∣ ¬p

Logical Valuesw∶∶=v ∣ F (w) ∣ HeapSel (H, `, w)

Syntactic Type Terms

U∶∶=

Heap Bindings

ĥ

∶∶=

∀[A; L; H] W1 → W2 ∣ A ∣ Null ∣ Ref ` ∣ Ref `˜ ∣ Arr (T )(` ↦ x ∶ T ) ∣ (` ↦ ⟨x ∶ T , `′ ⟩) ∣ (`˜ ↦ θ) ∣ ĥ1 ⊕ ĥ2 ∣ ∅Thaw Statesθ∶∶=

frzn ∣ thwd `WorldsW∶∶=

x ∶ T / Σ̂x, y, z∈Identifiers

Heaps

Σ̂

∶∶=

(H, ĥ)a∈

LocationConstants

Strong Locations

`
`˜

∶∶=

a ∣ L

r

∈

∶∶=

ã

F

∈

Weak Locations

A, B

∈

TypeVariables

H∈

HeapVariables

DynamicHeapLocations

L∈

LocationVariables

LogicalFunctionSymbols

P∈

LogicalPredicateSymbolsc ∈ ValueConstants ⊃ { true, false, null, undefined, 1, 2, “hanna”, (==), !, typeof, get, getElem, fix }Figure 7. Syntax of System !Dadditionally records a prototype link `′ . The binding (`˜ ↦ θ)
˜ to help
records the current thaw state of weak location `,maintain the invariant that it has at most one thawed location
at a time. We abuse the notation (H, ĥ1 ) ⊕ ĥ2 to mean(H, ĥ1 ⊕ ĥ2 ).
Uninterpreted Heap Symbols. To describe invariants about
the deep part of a heap, System !D introduces two uninterpreted heap symbols. The predicate HeapHas(H, `, k)represents the fact that the chain of objects in H starting with ` has the key k. Similarly, the function symbol
HeapSel (H, `, k) refers to the value retrieved when looking
up key k in the heap H starting with `.

4.

Type Checking

In this section, we discuss the well-formedness, typing, andsubtyping relations of System !D. The type system reuses the
System D [9] subtyping algorithm to factor subtyping obligations between a first-order SMT solver and syntactic subtyping rules. The novel technical developments here are: theformulation of flow-sensitive heap types in a dependent setting; the use of uninterpreted heap symbols to regain precision in the presence of imperative, prototype-based objects;
the encoding of array primitives to support idiomatic use of
JavaScript arrays; and the use of refinement types to assign
precise types to JavaScript operators.
Environments. The type checking relations make use oftype environments Γ and heap environments Σ.
Γ ∶∶= ∅ ∣ Γ, x ∶ T ∣ Γ, p ∣ Γ, A ∣ Γ, L ∣ Γ, H ∣ Γ, (`˜ ↦ ⟨T, `⟩)Σ ∶∶= (H, h)h ∶∶= ∅ ∣ h1 ⊕ h2 ∣ (` ↦ v) ∣ (` ↦ ⟨v, `′ ⟩) ∣ (`˜ ↦ θ)

A type environment binding records either: the derived typefor a variable; a formula p to track control flow along a
conditional branch; a polymorphic variable introduced by afunction type; or the description of a weak location (which
does not change flow-sensitively), namely, that every object
stored at `˜ satisfies type T and has prototype link `. A heap
environment is just like a heap type, except a strong location` binds the value v it stores (as opposed to the type of v).
4.1

Well-Formedness

As usual in a refinement type system, we define wellformedness relations (see [7]) that govern how values may
be used inside formulas. The key intuition is that formulas
are boolean propositions and mention only variables that are
currently in scope. Locations in a heap type Σ̂ must either
be location constants or location variables bound by the typeenvironment, and may not be bound multiple times. All heap
binders may refer to each other. Thus, the values in a heap
can be regarded as a dependent tuple. For the input world
x1 ∶T1 / Σ̂1 of a function type, the binder x1 and the bindersin Σ̂1 may appear in the output world W2 .
4.2

Subtyping

Several relations (see Figure 8 and [7]) comprise subtyping.
Subtyping and Implication. As in System D, subtyping on
refinement types reduces to implication of refinement formulas, which is discharged by a combination of uninterpreted,first-order reasoning and syntactic subtyping. Our treatmentof existential types follows the algorithmic (decidable) approach in [25]. In particular, when on the left side of an
obligation, the S-E XISTS rule adds the existential binding
to the environment; there is no support for existentials on

[U-N ULL ][U-W EAK R EF ]ty(c) is defined in the standard prelude files (basics.dref,
objects.dref, and prelude.dref). The standard T-VAR
rule assigns singleton types to variables. The rule T-F UN
uses the procedure HeapEnv that takes a “snapshot” of the
input heap type Σ̂1 by collecting all of its binders z ∶S to add
to the type environment and producing a heap environment
Σ1 for type checking the body. Dually, the world satisfaction
judgement Γ1 ⊢ T2 /Σ2 ⊧ W2 (defined in [7]) checks thatthe resulting type and heap environment T2 /Σ2 satisfies W2 ,modulo permutation of heap bindings.

Γ ⊢ Null <∶ Ref `˜Γ ⊢ Ref `˜ <∶ Ref `˜

4.4

Γ ⊢ T1 ⊑ T2

Subtyping[S-R EFINE ]y fresh[S-E XISTS ]Γ, p[y/x] ⇒ q[y/x]Γ ⊢ {x ∣ p} ⊑ {x ∣ q}

Γ, x ∶ T ⊢ S1 ⊑ S2
Γ ⊢ ∃x ∶ T . S1 ⊑ S2
Γ ⊢ U1 <∶ U2

Syntactic Subtyping (selected rules)[U-A RRAY ][U-VAR ][U-S TRONG R EF ]

Γ ⊢ Arr (T ) <∶ Arr (T )Γ ⊢ A <∶ A

Γ ⊢ Ref ` <∶ Ref `Figure 8. Subtyping for System !DΓ; Σ ⊢ v ∶∶ T

Value Typing (selected rules)
Γ(x) = S[T-C ONST ]Γ; Σ ⊢ c ∶∶ ty(c)Γ; Σ ⊢ x ∶∶ {y ∣ y = x}

[T-VAR ][T-F UN ]Γ⊢U
U = ∀[A; L; H] x ∶ T1 / Σ̂1 → W2
HeapEnv(Σ̂1 ) = (z ∶ S, Σ1 )
Γ1 = Γ, A, L, H, x ∶ T1 , z ∶ S
Γ1 ; Σ1 ⊢ e ∶∶ T2 /Σ2Γ1 ⊢ T2 /Σ2 ⊧ W2
Γ; Σ ⊢ λx. e ∶∶ {y ∣ y ∶∶ U }Figure 9. Value type checking for System !Dthe right. The way in which type checking introduces existentials guarantees that they always appear on the left.
References and Arrays. As in Alias Types [32], we enforce the invariant that distinct strong locations do not alias,
so references to them are never related by subtyping. In contrast, weak locations describe zero or more locations, and
it is safe to treat null as a subtype of any weak location(U-N ULL). That is, weak references are nullable but strong
ones are not. Arrays are invariant in their type parameter (UA RRAY), as usual, but can be related with additional predicates. For example, {ν ∶∶ Arr (Int)∧len(ν) = 2} is a subtypeof {ν ∶∶ Arr (Int)}.
Heaps. The heap subtyping judgement (defined in [7]) relates two heap types (H1 , ĥ1 ) and (H2 , ĥ2 ) if: (1) the heaps
agree on the “deep” part, that is, if H1 = H2 ; (2) the structureof the “shallow” parts ĥ1 and ĥ2 match modulo permutation;and (3) the heap bindings in ĥ1 and ĥ2 , which can be thoughtof as dependent tuples, are related by subtyping.
4.3

Value Typing

The value typing judgement Γ; Σ ⊢ v ∶∶ T (defined in
Figure 9 and [7]) verifies that the value v has type T in
the given environments. Since values do not produce any
effects, this judgement does not produce an output heap
environment. Each primitive constant c has a type, denotedby ty(c), that is used by T-C ONST. In our implementation,

Expression Typing

The expression typing judgement Γ; Σ ⊢ e ∶∶ T /Σ′ (inFigure 10 and [7]) verifies that the evaluation of expression e
produces a value of type T and a new heap environment Σ′ .
We write U as shorthand for the type {ν ∶∶ U }, and Σ ≡ Σ′
for heap equality modulo permutation of bindings.
Prenex Quantified Types. The T-L ET rule uses an existential to describe the type T1 of the variable x that goes out of
scope after the body expression is checked. Alternatively, themore traditional approach (e.g., [9]) requires that the variable
be eliminated (e.g., via subsumption), but we use existentials
because it simplifies several other typing rules.
So that existentials appear only on the left side of subtyping obligations, we ensure that the typing rules derive prenex
quantified types of the form ∃x∶T . S, where all the types T
and S are refinement types, not existential types. In particular, to combine the worlds of two branches, the Join operator (defined in [7]), rearranges existentials to ensure that theresulting world is in prenex form. For example, for a conditional with guard b, the join of (∃x1 ∶T1 . Top /(` ↦ x1 )) and(∃x2 ∶T2 . Top /(` ↦ x2 )) is (∃y ∶T12 . Top /(` ↦ y)) where○
T12 = {if b then T1 (ν) else T2 (ν)}.
Imperative Operations. We use two kinds of reference
cells in System !D: simple references that store base values and functions without prototype links, and object references that store dictionaries paired with prototype links.
We require that all imperative operations go through strong
locations. We do not need weak, simple locations since theycannot appear in DJS programs and they are not needed for
desugaring; and we do not need weak, object locations because we can use our thawing mechanism instead.
Three rules manipulate simple references. To check thereference allocation ref ` v, the rule T-R EF ensures that ` is
not already bound in the heap, and then adds a binding thatrecords exactly the value being stored. The rule T-D EREF
checks that the given value is a reference to a simple location, and then retrieves the stored value; this is the imperative
analog to the “selfifying” T-VAR rule. The rule T-S ETREF
strongly updates a simple location.
The rule T-N EW O BJ stores the dictionary v1 in the heap
at location `1 along with a prototype link to the location `2
that v2 refers to. Although no typing rules manipulate object
locations, several primitives (getElem, setElem, etc.) do.

Γ; Σ ⊢ e ∶∶ T /Σ′Expression Typing (selected rules)Γ; Σ ⊢ v ∶∶ T
[T-VAL ]Γ; Σ ⊢ v ∶∶ S

Γ; Σ ⊢ e1 ∶∶ T1 /Σ1Γ; Σ ⊢ v ∶∶ T /ΣΓ, x ∶ T1 ; Σ1 ⊢ e2 ∶∶ T2 /Σ2Γ; Σ ⊢ let x = e1 in e2 ∶∶ ∃x ∶ T1 . T2 /Σ2Γ, truthy(v); Σ ⊢ e1 ∶∶ T1 /Σ1Γ, falsy(v); Σ ⊢ e2 ∶∶ T2 /Σ2[T-L ET ]T /Σ′ = Join(v, T1 /Σ1 , T2 /Σ2 )[T-I F ]′Γ; Σ ⊢ if v then e1 else e2 ∶∶ T /Σ` ∉ dom(Σ)[T-R EF ][T-S ETREF ]Γ; Σ ⊢ v ∶∶ T

Σ′ = Σ ⊕ (` ↦ v)

Γ; Σ ⊢ ref ` v ∶∶ Ref `/Σ′Γ; Σ ⊢ v ∶∶ Ref `Σ ≡ Σ0 ⊕ (` ↦ v ′ )Γ; Σ ⊢ deref v ∶∶ {y ∣ y = v ′ }/Σ

[T-D EREF ]Γ; Σ ⊢ (v1 , v2 ) ∶∶ (Ref `, T )Σ ≡ Σ0 ⊕ (` ↦ v)
Σ′ = Σ0 ⊕ (` ↦ v2 )`1 ∉ dom(Σ)Γ; Σ ⊢ (v1 , v2 ) ∶∶ (Dict, Ref `2 )
Σ ≡ Σ0 ⊕ (`2 ↦ ⟨v ′ , `3 ⟩)Σ′ = Σ ⊕ (`1 ↦ ⟨v1 , `2 ⟩)Γ; Σ ⊢ v1 ∶= v2 ∶∶ {x ∣ x = v2 }/Σ′Γ; Σ ⊢ newobj `1 v1 v2 ∶∶ Ref `1 /Σ′[T-N EW O BJ ]Γ; Σ ⊢ v1 ∶∶ ∀[A; L; H] W1 → W2

Γ; Σ ⊢ v2 ∶∶ T2
Γ ⊢ [T /A]Γ ⊢ [m/M ]Γ ⊢ [Σ̂/H]′′′′′
W2 = Freshen(W2 )(W1 , W2 ) = Unroll(HInst(LInst(TInst((W1 , W2 ), A, T ), L, `), H, Σ̂))Γ ⊢ T2 /Σ ⊧ W1′ ; πW1′ = x ∶ T11 / Σ̂11
π ′ = π[v2 /x]
π ′ W2′′ = x′ ∶ T12 / Σ̂12
HeapEnv(Σ̂12 ) = (y ∶ S, Σ12 )[T-A PP ]Γ; Σ ⊢ [T ; `; Σ̂] v1 v2 ∶∶ ∃x′ ∶ T12 . ∃y ∶ S. {z ∣ z = x′ }/Σ12

Figure 10. Expression type checking for System !D

Unroll(HeapHas((H, ĥ), `, k)) = UnrollHas(H, ĥ, `, k)
UnrollHas(H, ĥ, `, k) =⎧has(d, k) ∨ UnrollHas(H, ĥ, `′ , k) if (` ↦ ⟨d ∶ T , `′ ⟩) ∈ ĥ⎪⎪⎪
⎨ HeapHas(H, `, k)else if ` ≠ ○⎪⎪⎪else (i.e., ` = ○)⎩ falseUnroll(ψ(HeapSel ((H, ĥ), `, k))) = UnrollSel(ψ, H, ĥ, `, k)
UnrollSel(ψ, H, ĥ, `, k) =⎧⎪ite has(d, k) ψ(sel (d, k)) (UnrollSel(ψ, H, ĥ, `′ , k))
⎪
⎪
⎪
⎪
⎪
if (` ↦ ⟨d ∶ T , `′ ⟩) ∈ ĥ⎨⎪ψ(HeapSel (H, `, k))else if ` ≠ ○
⎪
⎪
⎪
⎪
⎪
ψ(undefined)
else (i.e., ` = ○)⎩Figure 11. Heap unrolling
Function Application. To type check [T ; m; Σ̂] v1 v2 , the
T-A PP rule must perform some heavy lifting. Three wellformedness checks ensure that the number of type, location,and heap parameters must match the number of type, location, and heap variables of the function type, and that thesequence of locations ` contains no duplicates to ensure thesoundness of strong updates [32]. The procedure Freshen
generates fresh binders for the output world so that bindings
at different call sites do not collide.
The substitution of parameters for polymorphic variables
proceeds in three steps. First, the type variables A inside hastype predicates are instantiated with the type parameters T
using the procedure TInst. Second, the location variables L
are replaced with the parameters ` by ordinary substitution.
Third, the heap variables H are instantiated with heap parameters using a procedure HInst that substitutes heap bind-ings for heap variables. As a result, HeapHas and HeapSel
may refer to arbitrary heaps rather than just heap variables,
as required. These pre-types (and pre-formulas, pre-heaps,etc.) are expanded using the procedure Unroll, defined in
Figure 11, that transitively follows prototype links in heap
bindings, precisely matching the semantics of object key
membership and lookup. We write the location ○ for the rootof the prototype hierarchy. We use the notation ψ(p) to referto a formula context ψ, a formula with a hole, filled with p.
At this point, the polymorphic variables have been fully
instantiated. Next, the argument type T2 and current heap Σare checked to satisfy the input world x∶T11 / Σ̂11 . If so, thesubstitution π maps binders from the input heap Σ̂11 to thecorresponding ones in the current heap Σ. The substitution
is extended with a binding from x to the argument v2 andapplied to the output world. Then, like in the T-F UN rule, we
use HeapEnv to collect the bindings y ∶S in Σ̂12 and convert
it to a heap environment Σ12 . Finally, the derived type uses
existentials to describe the values in the output world.
Thaw and Freeze. To safely allow a weak, object location`˜ to be treated temporarily as strong, System !D ensures that`˜ has at most one corresponding thawed location ` at a time
(if there is none, we say `˜ is frozen) by recording its thaw
state — either thwd ` or frzn. One interesting aspect of ourformulation is that, to facilitate idiomatic programming, wechoose to allow the use of possibly-null references. Instead,to require that all references be provably non-null before
use, we can simply update the type signatures for object
primitives. We omit the typing rules for thawing and freezing
from Figure 10; we refer the reader to [7] for more details.
Location Polymorphism. To simplify the presentation of
System !D in this paper, we have limited location polymor-

phism in two ways. First, we allow location variables L torefer only to strong locations. In [7], we describe how to
add weak location polymorphism to function types and update the typing rules appropriately. Second, we offer onlya single mechanism — namely, universal quantification —to abstract over both simple locations as well as object locations. As a result, functions must be quantified over all
simple locations inserted by desugaring (to model imperative JavaScript variables), which clutters function types and,worse, requires explicit declaration and instantiation of locations that are “internal” to the desugaring translation andnot accessible in the original DJS program. Instead, in [7],we show how to use existential quantification in the output
types of functions to describe simple locations, and use universal quantification in the input types of functions only todescribe object locations, which are visible in DJS.
4.5

Type Soundness

Many standard stuck states are not stuck in JavaScript: afunction can be applied with any number of arguments; anoperator can be used with any values because of implicit
coercion; and, all property lookups succeed (possibly producing undefined). Nonetheless, several (non-exceptional)
stuck states remain: applying a non-function value; and retrieving a property for a non-object value. System !D is designed to ensure that well-typed programs do not get stuckand can only fail with exceptions due to retrieving a property
from undefined or null. We can also provide the stronger
guarantees that only bound keys are retrieved and only nonnull objects are accessed (thus ruling out the possibility ofnull dereference exceptions) simply by changing the typesof object primitives appropriately.
We expect that System !D satisfies progress and preservation theorems, but we have not yet proven them. The process will likely be tedious but not require new proof techniques. Unlike System D, which introduced the problematic nesting of syntactic types inside uninterpreted formulas,
System !D does not introduce any new mechanisms in therefinement logic. Furthermore, several variations of Alias
Types [23, 32, 37], even in a dependent setting [31], havebeen proven sound, and we expect to re-use their techniques
to prove the soundness of System !D.

5.

Desugaring DJS to System !D

In Figure 12, we present a selection of the explicitly typed
abstract syntax of DJS along with desugaring rules ⟪ e ⟫ = ethat translate DJS expressions e to System !D expressions e.
Most of the desugaring rules follow λJS [21] closely, so welimit our discussion to the aspects most relevant to DJS; werefer the reader to [7] and their work for more details. We use○
the metavariable I = [T ; m; Σ̂] to range over instantiation
parameters for function application. Instantiation parameters
are usually inferred by the type checker (§6).

Desugaring (selected rules)

⟪e⟫=e

⟪c⟫=c

[DS-C ONST]⟪ x ⟫ = deref x[DS-D EREF]⟪ e1 = e2 ⟫ = ⟪e1 ⟫ ∶= ⟪e2 ⟫′[DS-S ETREF]′⟪ var x = e; e ⟫ = let x = ref ax ⟪e⟫ in ⟪e ⟫[DS-R EF]⟪ /∗ ∶ I ∗ / e1 [e2 ] ⟫ =/∗ ∶ I ∗ / getElem (⟪e1 ⟫, ⟪e2 ⟫)[DS-G ET E LEM]

⟪ /∗ ∶ I ∗ / e1 [e2 ] = e3 ⟫ =/∗ ∶ I ∗ / setElem (⟪e1 ⟫, ⟪e2 ⟫, ⟪e3 ⟫)[DS-S ET E LEM]

⟪ /∗ ∶ I ∗ / delete e1 [e2 ] ⟫ =/∗ ∶ I ∗ / delElem (⟪e1 ⟫, ⟪e2 ⟫)[DS-D EL E LEM]

⟪ /∗ ∶ I ∗ / e2 in e1 ⟫ =/∗ ∶ I ∗ / hasElem (⟪e1 ⟫, ⟪e2 ⟫)[DS-H AS E LEM]

⟪ /∗ ∶ ` ∗ / { ek ∶ ev } ⟫ =[DS-O BJ L IT]
newobj ` {⟪ek0 ⟫ ↦ ⟪ev0 ⟫ ++ ⋯ } (pro(Object))⟪ /∗ ∶ ` ∗ / [ e ] ⟫ =newobj ` {“0” ↦ ⟪e0 ⟫ ++ ⋯ } (pro(Array))[DS-A RR L IT]⟪ /∗ ∶ I ∗ / e(e1 , . . . , en ) ⟫ =[DS-F UNC C ALL]/∗ ∶ I ∗ / 2⟪e⟫7 (window, (⟪e1 ⟫, . . ., ⟪en ⟫))⟪ /∗ ∶ I ∗ / e[e′ ](e1 , . . . , en ) ⟫ =let obj = ⟪e⟫ inlet m = getElem (obj , ⟪e′ ⟫) in/∗ ∶ I ∗ / 2m7 (obj , (⟪e1 ⟫, . . ., ⟪en ⟫))[DS-M ETH C ALL]⟪ new /∗ ∶ `new I ∗ / e(e1 , . . . , en ) ⟫ =let foo = ⟪e⟫ in
let obj = newobj `new {} (foo “prototype”) in/∗ ∶ I ∗ / 2foo7 (obj , (⟪e1 ⟫, . . ., ⟪en ⟫))⟪ /∗ ∶ I ∗ / e.apply(e1 , . . . , en ) ⟫ =/∗ ∶ I ∗ / 2⟪e⟫7 (⟪e1 ⟫, (⟪e2 ⟫, . . ., ⟪en ⟫))[DS-N EW]

[DS-A PPLY]

Figure 12. Desugaring DJS to System !D
The DS-C ONST rule for constants, the three DS-*R EF
rules for mutable variables, and the four DS-*E LEM rules
for object and array operations are straightforward.
Object Literals. In the rules DS-O BJ L IT and DS-A RR L IT,○
we write pro(e) = getProp (⟪e⟫, “prototype”) to set
the prototypes of fresh object and array literals, translated
to newobj which creates values with prototype links. Our
implementation inserts a fresh location if none is provided.
Function Application. The last four rules in Figure 12
handle different kinds function calls in JavaScript. The rules
DS-F UNC C ALL and DS-M ETH C ALL desugar “direct calls”○
and “method calls”, where 2e7 = getElem (e, “ code ”).
Notice that non-receiver arguments are packed into a single“arguments” tuple. In DS-F UNC C ALL, we write window for
the “global object” supplied as the receiver for direct calls.
The DS-N EW rule handles object construction by creating a
fresh object with newobj whose prototype is set to the object
in the constructor object’s “prototype” field, and calls thefunction in the “ code ” field to finish the initialization.

JavaScript provides two native functions apply and callin Function.prototype that allow the caller to explicitly
supply the receiver argument. We do not provide general
support apply and call in DJS, because they require mechanisms beyond the scope of our (already-large) type system; for example, the latter accepts an arbitrary number ofarguments. The primary benefit of (non-constructor) functions as objects in JavaScript is that they inherit apply andcall from Function.prototype, but since we do not support them, we sacrifice little expressiveness if the type system treats every non-constructor function as a scalar function value, rather than an object with the function storedin “ code ”. Furthermore, we can then support the limited use of apply required for our recursive function idiomsin § 2.7 using the rule DS-A PPLY that syntactically looks
for “apply” and explicitly sets the receiver. Because thetype systems prohibits (non-constructor) functions from being used as objects, there is no danger that the apply be“hijacked” by overwriting the “apply” property.
Control Operators. Throughout the paper, we wrote only
JavaScript functions that have either a single return statement or a return statement along every control flow path.
In general, however, return statements — as well as looping constructs and other control operators — can appear in
arbitrary positions. In System !D, we handle the general caseusing break and label expressions, following λJS [21]. We
omitted the formulation from our presentation for ease of
exposition; see [7] for details.

6.

Evaluation

In this section, we describe our implementation, the benchmarks we have annotated and type checked so far that
demonstrate the expressiveness of DJS, and identify several
ways for future work to improve the tool.
6.1

Implementation

We have implemented a type checker for DJS, available atravichugh.com/djs, that is currently approximately 6,600(non-whitespace, non-comment) lines of OCaml code. We
borrow the λJS [21] JavaScript parser, use their desugaring as a starting point for our own, and use the Z3 SMT
solver [11] to discharge logical validity queries. We specify
the System !D primitive functions in the files basics.dref
and objects.dref, and JavaScript built-in functions like
Object.prototype.hasOwnProperty in prelude.js(desugared to prelude.dref). These three files comprisea standard prelude included with every desugared DJS program for type checking.
Local Inference. Function definitions require explicit type
annotations, and we employ bidirectional type checking [29]techniques to infer types for local expressions. At a function
application, we infer missing type and location parameters
by “greedily” matching the types of arguments against any

Adapted Benchmark
JS: The Good Parts
prototypal
pseudoclassicalfunctional
parts
SunSpiderstring-fasta
access-binary-trees
access-nbody
V8
splay
Google Closure Library
typeOfOther
negatepassengers
counter
dispatch
TotalsUn

Ann

Queries

Time

18
15
19
11

36
23
43
20

731
706
862
605

2
2
8
3

10
34
129

18
50
201

263
2389
4225

1
23
39

17

36

571

1

15

31

1975

52

9
9
16
4
306

9
19
24
8
518

296
310
272
219
13424

1
3
1
1
137

Figure 13. Benchmarks (Un: LOC without annotations;Ann: LOC with annotations; Queries: Number of Z3 queries;
Time: Running time in seconds)
Arr (T ) and Ref L type terms in the the declared input typeand input heap. Because these type terms are invariant intheir parameters (recall the U-A RRAY and U-S TRONG R EF
rules from Figure 8), the greedy choice is always the rightone. For a function type with exactly one heap variable H(like all the ones we have encountered) and input heap type
(H, ĥ), we infer the corresponding heap argument by simply
collecting all locations in the current heap environment that
do not match the explicit location bindings in ĥ. In ourbenchmarks, we are able to omit most type and locationarguments and all heap arguments.
6.2

Benchmarks

To demonstrate the expressiveness of DJS, we have annotated and checked several small examples — inspired by
JavaScript: The Good Parts [10], the Google Closure Library [19], and the SunSpider [34] and V8 [20] benchmarks— that exercise a variety of invariants, besides those demonstrated by previous examples (e.g., negate, passengers,etc.). We also ported the counter and dispatch examples
from System D [9] to DJS to demonstrate the nesting offunction types inside objects with dynamic keys. Figure 13
summarizes our results, where for each example: “Un” is thenumber of (non-whitespace, non-comment) lines of code in
the unannotated benchmark; “Ann” is the lines of code in the
annotated DJS version (including comments because they
contain annotations); “Time” is the running time rounded to
the nearest second, tested on a 2.66GHz machine with 4GBof RAM running Ubuntu; and “Queries” is the number ofvalidity queries issued to Z3 during type checking.
Expressiveness. We highlight some of the features of DJS
that our benchmarks leverage. Besides the prototypal patterndiscussed in § 2.5, Crockford [10] presents three additionalinheritance patterns using JavaScript’s construction mechanism. Each of these examples relies on the support for imperative, prototype-based objects in DJS.
The behavior of the typeOf function is like the typeof
operator except that it returns the more informative result“null” for null and “array” for arrays; the operator returns “object” in both cases. The type specification for
typeOf depends on the ability to express intersections offunction types in DJS, and verifying it requires control-flow
tracking in the presence of mutation as well as a precise
specification for the native (ES5) function Array.isArray,
which we model in prelude.js.
The makeCumulative function in string-fasta.js iterates over an object with an unknown number of keys thatall store integers, and sums them in place within the object.
While iterating over the keys of the object, the function uses
a variable to store the key from the previous iteration, a subtle invariant that DJS is able to express by describing theheap before and after each iteration. Compared to the original version, we allow the bindings to store arbitrary values
and use a tag-test to sum only the integer bindings. To specify the original version requires universally quantified formulas, which DJS avoids to retain decidable type checking.
The splay benchmark defines the following interesting
tree node constructor. Rather than initializing each “own”
object with null left and right subtrees, the constructor’s
prototype object stores the defaults.
function Node(k,v) { this.k = k; this.v = v; }Node.prototype.left = null;Node.prototype.right = null;

After construction, however, Nodes are often extended with
explicit subtrees. Using the flexibility of refinements, we assign each Node a type with the predicate has(ν, “left”) ⇒˜ where `˜ is the weak location thatsel (ν, “left”) ∶∶ Ref `,describes Nodes, to ensure that retrieving the “left” key
produces another Node regardless of whether it is stored on
the object or not (and similarly for “right”).
Our largest example is access-nbody, which defines aconstructor function NBodySystem that creates a container
object to store an array of Body objects. The prototypesof both constructors are augmented with methods, and thethaw/freeze mechanism is heavily used while iterating over
the array of Body objects to read and write their fields.
6.3

Annotation Burden

As Figure 13 shows, our annotated benchmarks are approximately 1.7 times as large (70% overhead) as their unannotated versions on average. In our experience, a significant
majority of the annotation burden is boilerplate — unrelated
to the interesting typing invariants — that fall into the following five patterns. Our implementation includes preliminary support for automatically inserting several common
patterns of annotations by tracking a limited amount of type

information during desugaring (that require no changes totype checking). This effort has already significantly reduced
the annotation overhead, but there is plenty of room for further improvements in future work.
Closures. If a function refers to a variable from an outer
scope, its heap type must explicitly list its location and type.
In the following example, the desugarer uses the predictablelocations api and ae when desugaring pi and e, and thefunction type must contain the binding for api .
var pi = 3.14, e = 2.718;/*: Top /(api ↦ n ∶ Num) → Num /same */function getPi() { return pi; }To ease this burden, we collect the free variables in eachfunction definition and automatically add the corresponding
heap bindings that are missing. In situations where we cannot insert a suitably precise type for a location, we allow the
programmer to annotate a variable declaration var i = /∗ ∶T ∗ / e and we propagate T to functions that refer to i.
Loops. Because loops desugar to functions, they require aheap type annotation (like for arbitrary closures) to describe
invariants that hold before and after every iteration. We infer
heap types for basic patterns like the following.
/*: (ai ↦ {Int(ν) ∧ i ≥ 0}) ⊕ (asum ↦ Num)⊕ (ans ↦ Ref `)⊕ (` ↦ ⟨{ν ∶∶ Arr (Num) ∧ packed (ν)}, `′ ⟩) */for (i=0; i < ns.length; i++) { sum += ns[i]; }Thaw and Freeze. Every weak reference must first be
thawed before access, which quickly becomes burdensome.
As a simple aid, we surround an access to a weak reference with thaw and freeze operations, which is sufficient for
simple cases involving reads and weak updates. For more
complex invariants, like the relationship between accesses
to a weak reference (as in the passengers example from§ 2.7), a single thaw and freeze pair must surround both accesses. In the future, we plan to insert these operations atbasic block and function boundaries in the style of [31] sothat objects are tracked with strong references as long as
possible.
Untampered Natives. Functions that use JavaScript primitive functions like Object.prototype.hasOwnProperty
and Array.prototype.push and expect them not to be
overwritten, must explicitly constrain their input heaps as
such. In most cases, programmers expect natives to remain“untampered,” so desugaring could augment all function
types with these constraints.
Constructor Prototypes. The purpose of a constructor C is
to allow its instances to inherit properties of C.prototype(stored at location aCpro ), but functions like useC thatuse such an instance must then explicitly list the type ofC.prototype.

/*: #define TC {Dict(ν) ∧ ⋯ } *//*: #ctor this ∶ Ref /(this ↦ ⟨Emp, aCpro ⟩)→ {ν = this}/(this ↦ ⟨TC , aCpro ⟩) */function C() { ...; return this; }C.prototype.f = /*: Tf */ ...;
C.prototype.g = /*: Tg */ ...;/*: x ∶ Ref /(x ↦ ⟨TC , aCpro ⟩) ⊕(aCpro ↦ ⟨Tf (sel (ν, “f”)) ∧ Tg (sel (ν, “g”)), `op ⟩)→ Top /same */function useC(x) { ... x.f ... }This is a predictable pattern that should be easy to incorporate into desugaring, though we have not yet done so.
6.4

Performance

The running time of our type checker is acceptable for small
examples, but less so as the number of queries to the SMT
solver increases. We have not yet spent much effort to improve performance, but we have implemented a few optimizations that have already reduced the number of SMT
queries. First, even though desugaring works perfectly wellwithout any type information, we use DJS type annotations
to translate object and array operations to specific primitives, where possible, rather than the more general ones (e.g.,
getPropObj and getIdxArr rather than getElem) so thattype checking has fewer cases to try, and we insert type andlocation parameters so that they need not be inferred. Second, we modify the T-VAR rule, which normally assigns the“selfified” type {ν = x} to variable x that is already boundin Γ. Although this precision is crucial, the variable x often
has a simple syntactic type (e.g., Ref `) that is “hidden” behind the equality. Instead, if Γ(x) is of the form {ν ∶∶ U ∧ p},
we assign {ν ∶∶ U ∧ p ∧ ν = x} so that subsequent typing
rules can syntactically look for U rather than going throughadditional SMT queries as in the general case [9].
We expect that syntactically handling more common
cases will further improve performance. For example, eventhough the dynamic keys are crucial in certain situations,many examples use objects with finite and fixed key names,
which we should be able to handle with far fewer queries to
the SMT solver than in the current implementation.

7.

Conclusion and Future WorkIn this paper, we have shown how to scale up prior workon System D — a type system for dynamic languages in afunctional setting — to the real-world JavaScript setting —with imperative updates, prototype-based objects, and arrays— through a combination of strong updates and prototype
chain unrolling. We have demonstrated that our new system,
System !D, is expressive enough to support the invariantsfrom a series of small but varied examples drawn from existing JavaScript benchmarks. We have found that the fullrange of features in DJS are indeed required, but that many

examples fall into patterns that do not simultaneous exercise
all features. Therefore, we believe that future work on desugaring and on type checking can treat common cases speciallyin order to reduce the annotation burden and running time,and fall back to the full expressiveness of the system whennecessary. We believe that Dependent JavaScript is the mostpromising approach, to date, for supporting real-world dynamic languages like JavaScript.
Features for Future Work. DJS already supports a large
subset of JavaScript that can be used for projects where all
the code is controlled (e.g., server-side applications), andfuture work on integrating with run-time environments could
allow DJS code to run alongside full untyped JavaScript.
Next, we describe several features that we currently do notsupport, in addition to general use of apply and call as
discussed in §5.
To allow mutation of prototype links via the non-standard“ proto ” property, we could add a setproto expression
to the language and detect cycles during heap unrolling.
The eval statement allows a string to be parsed andexecuted, which is useful but dangerous if misused. Since
DJS is flow-sensitive, we can constraint eval with heap
invariants before and after the statement, and then perform
staged type checking in the style of [8] at run-time.
ES5 introduces optional per-object and per-property attributes (for example, to prevent modifications or deletions)that can likely be incorporated into our encoding of dictionaries. One benefit of such an extension is that the type system could reason more precisely about which objects are in a
prototype chain. For example, we could then allow non-arrayobjects to bind unsafe strings as long as we prevent themfrom appearing in the prototype chain of arrays, thus weakening the distinction we impose between array and non-arrayobjects (§ 2.6). A second benefit is that native objects could
be marked as unmodifiable, statically enforcing the patternthey are usually “untampered” as discussed in §6.
ES5 getters and setters interpose on object reads andwrites. Since this is a deep change to the semantics of object operations (invoking arbitrary functions), adding general
support for these will likely be heavyweight. Interestingly,
one can think of our treatment of the special array “length”
property (§2.6) as a built-in getter/setter.
Each function has an implicit arguments array that binds
all parameters supplied by the caller, regardless of how many
formals the function defines. Current ES6 proposals include
a modified version, where an explicit parameter can binda variable number of arguments beyond those named byformals, similar in style to Python.
The x instanceof Foo operator checks whether or not
Foo.prototype is somewhere along the prototype chain ofx. We could add a primitive to match these semantics.
Scalar values can be explicitly coerced by wrapper functions, such as Boolean, in addition to the implicit coercion
we have discussed.

Undesirable Features. The last three features we discuss regularly compete for the title of worst among several“warts” in the language (e.g., [10]) that lead to confusingcode and hard-to-detect bugs. Incidentally, the λJS translations of all three are straightforward and can be supported in
DJS, but we see no reason to given their demerits.
The with statement adds the fields of an object to thecurrent scope of a block, allowing them to be accessed without qualification. There is hardly a good reason to use thisfeature, and it is banned in ES5 “strict” mode.
All var declarations are implicitly lifted to the top of
the enclosing function, resulting in “function scope” rather
than lexical scope. Although simple to detect when varlifting kicks in, we opt for the latter. ES6 will likely add
an explicit let binding form that is not subject to lifting. In
DJS, var is essentially the new let form, but we stick withthe traditional syntax for familiarity.
For a “method call” x.f(y), the receiver x is supplied
for the this argument to the function, but for a “directcall” x(y), JavaScript implicitly supplies the global object
for this, masking common errors. We choose to staticallyreject direct calls to functions that require a this parameter.

8.

Related WorkIn this section, we discuss topics related to types for imperative dynamic languages, and hence strong updates and inheritance. The reader may refer to [9] for background on thechallenging idioms of even functional dynamic languages
and the solution that nested refinements provide.
Location Sensitive Types. The way we handle reference
types draws from the approach of Alias Types [32], in whichstrong updates are enabled by describing reference types
with abstract location names and by factoring reasoning into
a flow-insensitive tying environment and a flow-sensitive
heap. Low-level liquid types [31] employs their approach inthe setting of a first-order language with dependent types. In
contrast, our setting includes higher-order functions, and ourformulation of heap types gives variable names to unknown
heaps to reason about prototypes and gives names to all heap
values, which enables the specification of precise relationships between values of different heaps; the heap bindersof [31] allow only relationships between values in a single
heap to be described.
The original Alias Types work also includes support for
weak references that point to zero or more values, for whichstrong updates are not sound. Several subsequent proposals [2, 3, 14, 15, 31, 33] allow strong updates to weak references under certain circumstances to support temporary
invariant violations. We adapt the thaw/freeze mechanism
from [2] and [31] with mostly cosmetic changes.
Prototype Inheritance. Unlike early class-based languages,
such as Smalltalk and C++, the (untyped) language Self allows objects to be extended after creation and feature prototype, or delegation, inheritance. Static typing disciplines

for class-based languages (e.g., [1]) explicitly preclude object extension to retain soundness in the presence of width
subtyping, the ability to forget fields of an object. To mitigate the tension between object extension and subtyping,several proposals [6, 18] feature quite a different flavor: thefields of an object are split into a “reservation” part, which
may be added to an object but cannot be forgotten, and a“sealed part” that can be manipulated with ordinary subtyping. Our approach provides additional precision in two
important respects. First, we precisely track prototype hierarchies, whereas the above approaches flatten them into asingle collection of fields. Second, we avoid the separation ofreservation and sealed fields but still allow subtyping, since“width subtyping” in System !D is simply logical implication over refinement formulas; forgetting a field — discarding a has(d, k) predicate — does not imply that ¬has(d, k),which guards the traversal of the prototype chain.
Typed Subsets of JavaScript. Several (syntactic) type systems for various JavaScript subsets have been proposed.
Among the earliest is [35], which identifies silent errors that
result from implicit type coercion and the fact that JavaScript
returns undefined when trying to look up a non-existent
key from an object. The approach in [4] distinguishes between potential and definite keys, similar to the reservationand sealed discussed above; this general approach has been
extended with flow-sensitivity and polymorphism [39]. The
notion of recency types, similar to Alias Types, was applied
to JavaScript in [23], in which typing environments, in addition to heap types, are flow-sensitive. Prototype supportin [23] is limited to the finite number of prototype links
tracked by the type system, whereas the heap symbols in
System !D enable reasoning about entire prototype hierarchies. Unlike System !D, all of the above systems provide
global type inference; our system does not have principal
types, so we can only provide local type inference [29]. ADsafety [30] is a type system for ADsafe, a JavaScript sandbox, that restricts access to some fields. Although expressive
enough to check ADsafe, which heavily uses large object
literals, they do not support strong update and so cannot reason about object extension. Unlike System !D, none of theabove systems include dependent types, which are required
to express truly dynamic object keys and precise controlflow based invariants.
Recent work on JavaScript verification uses separation
logic [17] to track precise flow-sensitive invariants. They
support only first-order programs, and the expressiveness of
their logic takes them beyond automatic verification, thus
requiring properties to be manually proved.
JavaScript Semantics. We chose the JavaScript “semanticsby-translation” of λJS [21] since it targets a conventionalcore language that has been convenient for our study. An
alternate semantics [26] inherits unconventional aspects of
the language specification [24] (e.g., “scope objects”), which
complicates the formulation of static reasoning.

Acknowledgments
This work was supported by NSF Grants CCF-0644361,
CNS-0964702, and gifts from Microsoft Research. Part ofthis work was done while the first author was at Mozilla.

[19] Google. Closure library. https://developers.google.
com/closure/library.
[20] Google. V8 benchmark. http://v8.googlecode.com/
svn/data/benchmarks/.

References[21] A. Guha, C. Saftoiu, and S. Krishnamurthi. The Essence of
JavaScript. In ECOOP, 2010.

[1] M. Abadi and L. Cardelli. A Theory of Objects. SpringerVerlag, 1996.

[22] A. Guha, C. Softoiu, and S. Krishnamurthi. Typing Local
Control and State Using Flow Analysis. In ESOP, 2011.

[2] A. Ahmed, M. Fluet, and G. Morrisett. L3 : A Linear Languagewith Locations. Fundamenta Informaticae, 77(4), June 2007.

[23] P. Heidegger and P. Thiemann. Recency Types for Analyzing
Scripting Languages. In ECOOP, 2010.

[3] A. Aiken, J. Kodumal, J. S. Foster, and T. Terauchi. Checking
and Inferring Local Non-Aliasing. In PLDI, 2003.

[24] E. International.
ECMAScript Language Specification,
ECMA-262, 3rd ed. 1999.

[4] C. Anderson, S. Drossopoulou, and P. Giannini. Towards Type
Inference for JavaScript. In ECOOP, 2005.

[25] K. W. Knowles and C. Flanagan. Compositional Reasoning
and Decidable Checking for Dependent Contract Types. In
PLPV, 2009.

[5] G. M. Bierman, A. D. Gordon, C. Hritcu, and D. E. Langworthy. Semantic Subtyping with an SMT Solver. In ICFP, 2010.
[6] V. Bono and K. Fisher. An Imperative, First-Order Calculus
with Object Extension. In ECOOP, 1998.
[7] R. Chugh, D. Herman, and R. Jhala. Dependent Types for
JavaScript — Appendix. arxiv.org/abs/1112.4106.

[26] S. Maffeis, J. Mitchell, and A. Taly. An operational semantics
for JavaScript. In APLAS, 2008.
[27] J. McCarthy. Towards a Mathematical Science of Computation. In IFIP, 1962.
[28] B. C. Pierce. Types and Programming Languages. 2002.

[8] R. Chugh, J. A. Meister, R. Jhala, and S. Lerner. Staged
Information Flow for JavaScript. In PLDI, 2009.

[29] B. C. Pierce and D. N. Turner. Local Type Inference. In
POPL, 1998.

[9] R. Chugh, P. M. Rondon, and R. Jhala. Nested Refinements:
A Logic for Duck Typing. In POPL, 2012.

[30] J. G. Politz, S. A. Eliopoulos, A. Guha, and S. Krishnamurthi.
Adsafety: Type-based Verification of JavaScript Sandboxing.
In USENIX Security, 2011.

[10] D. Crockford. JavaScript: The Good Parts. Yahoo! Press,
2008.
[11] L. de Moura and N. Bjørner. Z3: An Efficient SMT solver. In
TACAS, 2008.
[12] R. DeLine and M. Fähndrich. Enforcing High-level Protocols
in Low-level Software. In PLDI, 2001.
[13] ECMA.
TC-39 Committee.
community.php.

www.ecmascript.org/[14] M. Fahndrich and R. DeLine. Adoption and Focus: Practical
Linear Types for Imperative Programming. In PLDI, 2002.
[15] J. Foster, T. Terauchi, and A. Aiken. Flow-sensitive Type
Qualifiers. In PLDI, 2002.
[16] M. Furr, J. hoon (David) An, J. S. Foster, and M. W. Hicks.
Static type inference for ruby. In SAC, 2009.
[17] P. Gardner, S. Maffeis, and G. D. Smith. Towards a Program
Logic for JavaScript. In POPL, 2012.
[18] P. D. Gianantonio, F. Honsell, and L. Liquori. A Lambda Calculus of Objects with Self-Inflicted Extension. In OOPSLA,
1998.

[31] P. Rondon, M. Kawaguchi, and R. Jhala. Low-Level Liquid
Types. In POPL, 2010.
[32] F. Smith, D. Walker, and G. Morrisett. Alias Types. In ESOP,
2000.
[33] J. Sunshine, K. Naden, S. Stork, J. Aldrich, and E. Tanter.
First-class State Change in Plaid. In OOPSLA, 2011.
[34] SunSpider. Javascript benchmark. http://www.webkit.
org/perf/sunspider/sunspider.html.
[35] P. Thiemann.
Towards a Type System for Analyzing
JavaScript Programs. In ESOP, 2005.
[36] S. Tobin-Hochstadt and M. Felleisen.
Untyped Languages. In ICFP, 2010.

Logical Types for[37] D. Walker and G. Morrisett. Alias Types for Recursive Data
Structures. In TIC. 2000.
[38] S. yu Guo and B. Hackett. Fast and Precise Hybrid Type
Inference for JavaScript. In PLDI, 2012.
[39] T. Zhao. Polymorphic Type Inference for Scripting Languages with Object Extensions. In DLS, 2011.