Type checking for JavaScript

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 type errors. Therefore, programmers can benefit from the flexible programming style offered by JavaScript and from the safety offered by a static type system. We demonstrate our type system with a formalism of JavaScript, JS₀. Our types are structural. Members of an object type are classified into definite and potential. A potential member becomes definite upon assignment. We outline a proof that our type system is sound.