A Trusted Mechanised Specification of the JavaScript Standard

Speaker: Philippa Gardner, Imperial College London

Abstract:

JavaScript is by far the most widely used web language for client-side applications. Whilst the development of JavaScript was initially led by implementations, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of the language, to serve as a trusted basis for high-assurance proofs of language properties, the compilation of high-level languages, and JavaScript implementations.

We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript. We present JSCert, a mechanised specification of ECMAScript 5 in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We establish trust in several ways: JSCert is designed to be `eyeball close' to ECMAScript 5; JSRef is provably correct with respect to JSCert; and JSRef is tested to industrial standard. We believe that, over time, our methodology will lead to a highly trusted specification of the JavaScript standard.

Biography:

Philippa Gardner is a professor in the Department of Computing at Imperial College London. Her current research focuses on program verification: in particular, reasoning about web programs (JavaScript and DOM) and reasoning about concurrent programs.

She completed her PhD thesis, supervised by Professor Gordon Plotkin at Edinburgh in 1992. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship from 2005 to 2010 at Imperial. She is the Director of the UK Research Institute in Automatic Program Analysis and Verification, funded by GCHQ in association with EPSRC.

Start time:
Location: MTV - 10 Forward
Duration: 1 hour 11 minutes
Channel: Main

Views since archived: 787

Small (640x380) Big (896x504)

WebM , Mpeg4
To download, right-click and select "Save Link As..."