Great stuff! I'm really glad to see this materialise. /Andreas
On 25 January 2014 20:15, Gareth Smith <[email protected]> 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 > [email protected] > https://mail.mozilla.org/listinfo/es-discuss _______________________________________________ es-discuss mailing list [email protected] https://mail.mozilla.org/listinfo/es-discuss
