Ah, this looks really neat! :D I wasn't familiar with any research on formalising JavaScript semantics besides λjs, so it's neat to see more research on this front :)
On 25 January 2014 22:55, Gareth Smith <[email protected]> wrote: > > Apologies if this is a duplicate - I tried sending this earlier, but it > didn't seem to go through. > > Gareth Smith <[email protected]> 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 > [email protected] > https://mail.mozilla.org/listinfo/es-discuss > -- -- Quildreen "(Soreλ\a)" Motta (http://robotlolita.github.io/<http://killdream.github.com/> ) *— JavaScript Alchemist / Minimalist Designer / PLT hobbyist —*
_______________________________________________ es-discuss mailing list [email protected] https://mail.mozilla.org/listinfo/es-discuss
