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
This talk is for a general audience, interested in the formalisation of
techniques of mechanised specification can handle the complexity of
We present JSCert, a mechansised specification of ECMAScript 5 in the
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
This work has recently been published in POPL'14. See http://jscert.org/
for more details.
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.
See http://www.doc.ic.ac.uk/~pg/ for more details.