JSCert: a JavaScript formalisation in the Coq theorem prover

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

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

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>

Thanks :)

G

Quildreen Motta <quildreen at gmail.com> writes:
> 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
>>

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