Recency types for dynamically-typed, object-based languages: Strong updates for JavaScript

Object-based languages with dynamic type systems are popular because they accelerate the development of short programs. As larger programs are built with those languages, static analyses become important tools for detecting programming errors. We define such an analysis as a type system for an imperative object-based calculus and prove its type soundness. The calculus models essential features of the JavaScript language, as an example of a typical and widely used dynamically-typed, object-based lan-guage. The model includes objects as property maps, type change during object initialization, and precise support for JavaScript’s prototype mechanism. As a more general technical contribution, our work demon-strates that the idea of recency abstraction can be transferred from abstract interpretation to a type system. We model recency infor-mation with a notion of precise object pointers that enables strong, type changing updates of object types during a generalized initial-ization phase. The same precise object pointers allow for an ac-curate treatment of the prototype mechanism. Unlike linear types, precise object pointers can be nested and mixed arbitrarily with or-dinary, imprecise object pointers in the type of a data structure. 1