A Trusted Mechanised JavaScript Specification

Martin Bodin 1, 2 Arthur Charguéraud 3, 4 Daniele Filaretti 5 Philippa Gardner 5 Sergio Maffeis 5 Daiva Naudziuniene 5 Alan Schmitt 1 Gareth Smith 5
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
4 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Communication dans un congrès
POPL 2014 - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. 2014
Liste complète des métadonnées


https://hal.inria.fr/hal-00910135
Contributeur : Arthur Charguéraud <>
Soumis le : mercredi 27 novembre 2013 - 14:02:40
Dernière modification le : jeudi 9 février 2017 - 15:57:54
Document(s) archivé(s) le : lundi 3 mars 2014 - 16:30:41

Fichier

jscert_popl.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 2014. <hal-00910135>

Partager

Métriques

Consultations de
la notice

1120

Téléchargements du document

406