An Operational Semantics for JavaScript

We define a small-step operational semantics for the ECMAScript standard language corresponding to JavaScript, as a basis for analyzing security properties of web applications and mashups. The semantics is based on the language standard and a number of experiments with different implementations and browsers. Some basic properties of the semantics are proved, including a soundness theorem and a characterization of the reachable portion of the heap.

• Type: Conference
• Year: 2008
• Where: APLAS
• Authors: Sergio Maffeis, John C. Mitchell, Ankur Taly
• Keywords: APLAS 2008, ECMAScript Standard Language, Language Standard, Programming Languages, Small-step Operational Semantics