Apologies if this is a duplicate - I tried sending this earlier, but it
didn't seem to go through.

Gareth Smith <gds at doc.ic.ac.uk> writes:

> We are pleased to announce JSCert, a formalisation of Chapters 8-14 of
> the ES5 standard. 
>
> We've built JSCert using the Coq proof assistant, using the same
> metaphors and data structures as the ES5 standard, and following ES5
> algorithm listings line-by-line. This means we can evolve our formalism
> along with ECMAScript: local changes to the standard should mean
> similarly local changes to JSCert. At the same time, we've structured
> JSCert to make it as easy as possible to build analysis and verification
> tools on top.
>
> We also provide JSRef, an interpreter for ES5, which we have verified in
> Coq to correctly implement JSCert. We have also tested JSRef using
> test262. Since each line of JSRef has a close correspondence with a
> given line of JSCert and the ES5 algorithms we will be able to use code
> coverage tools to begin to evaluate how much of ES5 is covered by
> test262.
>
> We very much hope that people will be interested in using JSCert and
> JSRef for investigating, for example, semantics-preserving compilation
> to ECMAScript, or other language analyses.
>
> You can find papers, code, talks and docs all at our website:
>
> http://jscert.org
>
> The code is here:
>
> http://github.com/jscert/jscert
>
> And our recent paper describing the project is here:
>
> http://www.doc.ic.ac.uk/~gds/jscert_popl14.pdf
>
> Thanks,
>
> Gareth

(duplicate message)