Paper Info
Title
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.
Year
DOI
Venue
2014
10.1145/2535838.2535876
POPL
Keywords
Field
DocType
javascript specification,coq proof,ecma standardisation process,language property,current ecma standard,ecma conformance test suite,ecma standard,mechanised specification,high-level language compilation,coq proof assistant,javascript implementation,javascript
Test suite,Programming language,Computer science,Unobtrusive JavaScript,Implementation,Mathematical proof,Interpreter,JavaScript,Proof assistant
Conference
Volume
Issue
ISSN
49
1
0362-1340
Citations 
PageRank 
References 
30
1.15
34
Authors
8
Name
Order
Citations
PageRank
Martin Bodin1474.28
Arthur Chargueraud2782.55
Daniele Filaretti3422.12
Philippa Gardner431414.45
Sergio Maffeis568533.25
Daiva Naudziuniene6322.21
Alan Schmitt754731.50
Gareth Smith8301.15