The Essence of JavaScript

TL;DR

This paper introduces a core calculus for JavaScript, capturing its peculiarities, and demonstrates its faithfulness and utility through real-world tests and a security type system.

Contribution

It presents a formal core calculus for JavaScript, models language peculiarities, and extends it with a security type system, bridging theory and practical application.

Findings

Faithful modeling of JavaScript peculiarities

Successful implementation of a security type system

Validation using real-world test suites

Abstract

We reduce JavaScript to a core calculus structured as a small-step operational semantics. We present several peculiarities of the language and show that our calculus models them. We explicate the desugaring process that turns JavaScript programs into ones in the core. We demonstrate faithfulness to JavaScript using real-world test suites. Finally, we illustrate utility by defining a security property, implementing it as a type system on the core, and extending it to the full language.