Recency Types for Analyzing Scripting Languages

With the current surge of scripting technologies, large programs are being built with dynamically typed languages. As these programs grow in size, semantics-based tools gain importance for detecting programming errors as well as for program understanding. As a basis for such tools, the authors propose a descriptive type system for an imperative call-by-value lambda calculus with objects. The calculus models essential features of JavaScript, a widely used dynamically-typed language: first-class functions, objects as property maps, and prototypes. The authors' type system infers precise singleton object types for recently allocated objects.