Gradual typing embedded securely in JavaScript

JavaScript’s flexible semantics makes writing correct code hard and writing secure code extremely difficult. To address the former prob-lem, various forms of gradual typing have been proposed, such as Closure and TypeScript. However, supporting all common pro-gramming idioms is not easy; for example, TypeScript deliberately gives up type soundness for programming convenience. In this pa-per, we propose a gradual type system and implementation tech-niques that provide important safety and security guarantees. We present TS?, a gradual type system and source-to-source compiler for JavaScript. In contrast to prior gradual type systems, TS? features full runtime reflection over three kinds of types: (1) simple types for higher-order functions, recursive datatypes and dictionary-based extensible records; (2) the type any, for dynami-cally type-safe TS? expressions; and (3) the type un, for untrusted