JSCert: a JavaScript formalisation in the Coq theorem prover

Quildreen Motta quildreen at gmail.com
Sat Jan 25 17:54:03 PST 2014


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 <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
> 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 —*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.mozilla.org/pipermail/es-discuss/attachments/20140125/718005ef/attachment.html>


More information about the es-discuss mailing list