Dependent types for JavaScript
- 19 October 2012
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 47 (10), 587-606
- https://doi.org/10.1145/2384616.2384659
Abstract
We present Dependent JavaScript (DJS), a statically typed dialect of the imperative, object-oriented, dynamic language. DJS supports the particularly challenging features such as run-time type-tests, higher-order functions, extensible objects, prototype inheritance, and arrays through a combination of nested refinement types, strong updates to the heap, and heap unrolling to precisely track prototype hierarchies. With our implementation of DJS, we demonstrate that the type system is expressive enough to reason about a variety of tricky idioms found in small examples drawn from several sources, including the popular book JavaScript: The Good Parts and the SunSpider benchmark suite.Keywords
Other Versions
This publication has 20 references indexed in Scilit:
- Fast and precise hybrid type inference for JavaScriptPublished by Association for Computing Machinery (ACM) ,2012
- Nested refinementsPublished by Association for Computing Machinery (ACM) ,2012
- Towards a program logic for JavaScriptPublished by Association for Computing Machinery (ACM) ,2012
- Polymorphic type inference for scripting languages with object extensionsPublished by Association for Computing Machinery (ACM) ,2011
- An Operational Semantics for JavaScriptLecture Notes in Computer Science, 2008
- Towards Type Inference for JavaScriptLecture Notes in Computer Science, 2005
- Towards a Type System for Analyzing JavaScript ProgramsLecture Notes in Computer Science, 2005
- Checking and inferring local non-aliasingPublished by Association for Computing Machinery (ACM) ,2003
- Adoption and focusPublished by Association for Computing Machinery (ACM) ,2002
- A lambda calculus of objects with self-inflicted extensionPublished by Association for Computing Machinery (ACM) ,1998