[PRL] [1112.4106] Dependent Types for JavaScript

[Mitchell Wand]

http://arxiv.org/abs/1112.4106

More from Jhala:

Dependent Types for JavaScript
Ravi Chugh <http://arxiv.org/find/cs/1/au:+Chugh_R/0/1/0/all/0/1>, Ranjit
Jhala <http://arxiv.org/find/cs/1/au:+Jhala_R/0/1/0/all/0/1>
(Submitted on 18 Dec 2011)

Dynamic languages like JavaScript, Python, and Ruby feature run-time
tag-tests, higher-order functions, extensible objects, and imperative
updates. In recent work on System D, we showed how to support many of these
features in a functional setting. In this work, we define a new calculus,
System !D (pronounced "D-ref"), that extends the previous one in two ways.
First, we add flow-sensitive heap types to reason about strong updates to
mutable variables. Second, we incorporate heap unrolling and uninterpreted
heap symbols to precisely reason about prototype-based objects. We
demonstrate that System !D is expressive by defining DJS, a large
JavaScript subset that translates to System !D for type checking. Through
several patterns advocated in the popular book JavaScript: The Good Parts,
we show that System !D is a practical typed intermediate language for
real-world, imperative dynamic languages with higher-order functions and
extensible, prototype-based objects.
-------------- next part --------------
HTML attachment scrubbed and removed