A trusted mechanised specification of javascript: One year on

0Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.

Abstract

The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL’14 and the current state of the project at CAV’15. We evaluate the work of POPL’14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google’s V8 Array library, enabling us to cover more of the language and to pass more tests.

References Powered by Scopus

An operational semantics for javaScript

76Citations
N/AReaders
Get full text

A trusted mechanised JavaSript specification

55Citations
N/AReaders
Get full text

Pretty-big-step semantics

45Citations
N/AReaders
Get full text

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Cite

CITATION STYLE

APA

Gardner, P., Smith, G., Watt, C., & Wood, T. (2015). A trusted mechanised specification of javascript: One year on. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9206, pp. 3–10). Springer Verlag. https://doi.org/10.1007/978-3-319-21690-4_1

Readers' Seniority

Tooltip

PhD / Post grad / Masters / Doc 2

67%

Researcher 1

33%

Readers' Discipline

Tooltip

Computer Science 3

100%

Save time finding and organizing research with Mendeley

Sign up for free