In this paper we first develop a formalism of JavaScript, JS0, and a static type system that will detect such type errors. Thus, programmers can benefit from the flexible programming style offered by JavaScript and from the safety offered by a static type system. Our types are structural and allow objects to evolve in a controlled manner by classifying members as definite or potential. A potential member becomes definite upon assignment. We prove soundness of our type system.
We then define a type inference algorithm for JS0 that is sound with respect to the type system. If the type inference algorithm succeeds, then the program is typeable. Therefore, programmers can benefit from the safety offered by the type system, without the need to write explicitly types in their programs.