Christopher Anderson and Paola Giannini

Type checking for JavaScript

In WOOD'04, 2004


JavaScript is a powerful imperative object based language made popular by its use in web pages. It supports flexible program development by allowing dynamic addition of members to objects. Code is dynamically typed: a runtime access to a non-existing member causes an error.

We suggest a static type system for JavaScript that will detect such runtime type errors. Therefore, programmers can have the benefit of flexible programming offered by JavaScript with the safety offered by a static type system.

We demonstrate our type system with a formalism of JavaScript, JS0. Our type system is based on structural recursive types. Members of a type are classified into definite and potential. The type of an object can evolve through assignment to potential members which turns them to definite. We first present the type system with integer and object types, and then add type variables to have polymorphism à la ML. We prove that our type system is sound.


[ bib | .pdf ]

Back


This file has been generated by bibtex2html 1.43