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 prconcurrencyesent 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.}
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.}
}
@Article{Calcagno2010Adjunct,
...
...
@@ -511,7 +511,7 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
@inproceedings{Raad2016Verifying,
Title={Verifying Concurrent Graph Algorithms},
Author={Azalea Raad and Aquinas Hobor and Jules Villard and Philippa Gardner},
Booktitle={Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},
Booktitle={Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS)},
