Type Checking for JavaScript

We demonstrate our type system with a formalism of JavaScript, JS0. 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.