[PRL] [1112.4106] Dependent Types for JavaScript

[Matthias Felleisen]

He sure knows how to write marketing prose. 



On Dec 22, 2011, at 8: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