A typed intermediate language for specifying the ECMAScript standard

11/14/2023

ECMA-SL é uma nova plataforma para a especificação e análise do ECMAScript standard. No núcleo desta plataforma está a ECMA-SL, uma nova linguagem intermédia desenhada para ser o mais semelhante possível à metalinguagem do ECMAScript standard. Com esta linguagem intermédia, a equipa do projeto ECMA-SL desenvolveu dois interpretadores de referência para a quinta e sexta versão do standard, ECMARef5 e ECMARef6, respetivamente. Ambos os interpretadores foram testados exaustivamente contra o Test262, o conjunto oficial de testes de conformidade para JavaScript, e constituem as implementações académicas mais completas do standard para as suas respetivas versões. Uma limitação importante da linguagem ECMA-SL é que não é tipificada, tornando os programas escritos em ECMA-SL extremamente difíceis de corrigir e refatorizar. Para atenuar este problema, introduzimos Typed ECMA-SL, uma extensão de ECMA-SL que adiciona tipificação estática com anotações de tipos opcionais. Typed ECMA-SL inclui um sistema de tipos estáticos para verificar a conformidade dos programas com as declarações de tipos e gera feedback intuitivo quando deteta erros. Formalizámos um subconjunto de Typed ECMA-SL, provando a consistência do sistema de tipos para o fragmento formalizado. Além disso, implementámos e tipificámos um interpretador simplificado de JavaScript com uma estrutura semelhante aos interpretadores de referência. Isto sugere que seremos capazes de tipificar completamente os interpretadores de referência, possibilitando a sua extensão para novas versões do ECMAScript standard. 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.

Authors in the community:

• 

  A

  André Filipe Ferreira do Nascimento

  ist192419

Supervisors of this institution:

• 

  J

  José Faustino Fragoso Femenin dos Santos

  ist153921

203837550

Mestrado em Engenharia Informática e de Computadores

electrical-engineering-electronic-engineering-information-engineering - Electrical engineering, electronic engineering, information engineering

Keywords

• ECMAScript
• ECMA-SL
• ECMARef6
• Typed ECMA-SL
• Type Declarations
• Type System
• Declarações de Tipos
• Sistema de Tipos

eng - English

Instituto Superior Técnico