JSCert: a JavaScript formalisation in the Coq theorem prover

Gareth Smith gds at doc.ic.ac.uk
Sat Jan 25 21:38:21 PST 2014


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
>>


More information about the es-discuss mailing list