Open Mechanized Foundations for JavaScript Regular Expressions
Category
Contribute
Institutions
EPFL
Data type
4D STEM data
Field
Materials Science
Researchers
Barrière, Aurèle
Description
The JavaScript programming language natively include regexes, the modern descendants of regular expressions. Many JavaScript programs rely on these regexes to match or extract patterns in text for a variety of applications. The behavior of these regexes is precisely described in a chapter of the paper-based, pseudocode JavaScript standard, ECMAScript. However, this standard is still far from the gold ORD standard for describing language semantics: a two-sided mechanized specification. In a mechanization, the specification is written in an interactive proof assistant like Coq/Rocq, enabling mechanized formal reasoning. Two-sided means that it can be used by implementers (to check their implementations) and by users (to reason about their programs). This project aims to contribute the first open mechanized, reusable, executable, two-sided mechanization for JavaScript regexes. We translated the regex chapter of the ECMAScript standard into the Coq/Rocq proof assistant. These definitions can be extracted to an executable reference implementation, that we used to validate the regex tests of the official JavaScript test suite. We demonstrated the usability of the mechanization by conducting mechanized proofs about JavaScript regex semantics.