quildreen at gmail.com
Sat Jan 25 17:54:03 PST 2014
Ah, this looks really neat! :D
besides λjs, so it's neat to see more research on this front :)
On 25 January 2014 22:55, Gareth Smith <gds at doc.ic.ac.uk> wrote:
> 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
> es-discuss mailing list
> es-discuss at mozilla.org
Quildreen "(Soreλ\a)" Motta
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the es-discuss