[PRL] [1112.4106] Dependent Types for JavaScript

[David Herman]

Ravi Chugh will be interning with us starting next month to work on types for JS. Hopefully Sam will be able to consult on the project from time to time, too.

Dave

On Dec 22, 2011, at 5:04 PM, Mitchell Wand wrote:

> http://arxiv.org/abs/1112.4106
> 
> More from Jhala:
> 
> Dependent Types for JavaScript
> 
> Ravi Chugh, Ranjit Jhala
> (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.
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl

-------------- next part --------------
HTML attachment scrubbed and removed