JSCert: a JavaScript formalisation in the Coq theorem prover

Andreas Rossberg rossberg at google.com
Tue Jan 28 14:26:01 PST 2014


Great stuff! I'm really glad to see this materialise.

/Andreas

On 25 January 2014 20:15, Gareth Smith <gds at doc.ic.ac.uk> wrote:
> 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
> _______________________________________________
> es-discuss mailing list
> es-discuss at mozilla.org
> https://mail.mozilla.org/listinfo/es-discuss


More information about the es-discuss mailing list