A Trusted Mechanised JavaScript Specification

Abstract : JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties. We present JSCert, a formalisation of the current ECMA standard in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We give a Coq proof that JSRef is correct with respect to JSCert and assess JSRef using test262, the ECMA conformance test suite. Our methodology ensures that JSCert is a comparatively accurate formulation of the English standard, which will only improve as time goes on. We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript.
Document type :
Conference papers
Complete list of metadatas

Cited literature [51 references]  Display  Hide  Download

https://hal.inria.fr/hal-00910135
Contributor : Arthur Charguéraud <>
Submitted on : Wednesday, November 27, 2013 - 2:02:40 PM
Last modification on : Thursday, October 3, 2019 - 2:04:02 PM
Long-term archiving on : Monday, March 3, 2014 - 4:30:41 PM

File

jscert_popl.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00910135, version 1

Citation

Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, et al.. A Trusted Mechanised JavaScript Specification. POPL 2014 - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. ⟨hal-00910135⟩

Share

Metrics

Record views

2783

Files downloads

753