A Typed Intermediate Language for Specifying the ECMAScript Standard

André Filipe Ferreira do Nascimento

Key information

Authors:

André Filipe Ferreira do Nascimento (André Filipe Ferreira do Nascimento)

Supervisors:

José Faustino Fragoso Femenin dos Santos (José Faustino Fragoso Femenin dos Santos)

Published in

11/14/2023

Abstract

ECMA-SL is a new platform for the specification and analysis of the ECMAScript standard. At the core of the ECMA-SL platform is ECMA-SL, a new intermediate language designed to be as close as possible to the meta-language of the ECMAScript standard. Using this intermediate language, the ECMA-SL team has developed two reference interpreters for the 5th and 6th versions of the ECMAScript standard, ECMARef5 and ECMARef6, respectively. Both interpreters were thoroughly tested against Test262, the official conformance test suite for JavaScript, and are currently the most complete academic implementations of the standard for their respective versions. An important shortcoming of the ECMA-SL language is that it is untyped, making ECMA-SL programs extremely difficult to debug and refactor. To address this issue, we introduce Typed ECMA-SL, an extension of ECMA-SL that adds static typing with optional type annotations to the language. Typed ECMA-SL comes with a static type system for verifying the adherence of programs to the supplied type declarations and provides user-friendly feedback when type errors occur. We formalized a subset of Typed ECMA-SL, proving the soundness of our type system for the formalized fragment. Additionally, we implemented and typed a simplified JavaScript interpreter with a similar structure to the reference interpreters. This suggests that we will be able to fully type the reference interpreters, enabling their extension to newer versions of the ECMAScript standard.