TeJaS: Retrofitting Type Systems for JavaScript
Abstract
JavaScript programs vary widely in functionality, complexity, and use, and analyses of these programs must accommodate such variations. Type-based analyses are typically the simplest such analyses, but due to the language’s subtle idioms and many application-specific needsranging from general-purpose program type-checking to verifying security properties to typing library usagewe have found that a single type system does not work well in all contexts. However, these different uses still share many common elements that can be extended and adapted for each setting.
In this paper we present TeJaS, a framework for building type systems for JavaScript. TeJaS has been engineered modularly to encourage experimentation. TeJaS reifies its initial type environment, allowing for easy modeling of the various execution contexts of JavaScript programs, and its type language and typing rules are extensible, allowing for variations of the type system to be constructed easily.
The paper presents the base TeJaS type system, which performs traditional type-checking for JavaScript. Because JavaScript demands complex types, we explain several design decisions to improve user ergonomics. We then describe TeJaS’s modular structure, and illustrate it by reconstructing the essence of a very different type system for JavaScript. Systems built from TeJaS have been applied to several real-world, third-party JavaScript programs.
Links
- Paper (ACM DL):
- Presentation:
- pptx
- Project page:
- available here
Contact
- Email (essential):
- (first initial + last name) {at} ccs.neu.edu
- Location (likely):
- West Village H, Office 326
- Post (possible):
-
Northeastern University
Khoury College of Computer Sciences
360 Huntington Ave, 2nd floor
Boston, MA 02115
