Azalea Raad has had two papers published in Programming Languages and System: Proceedings of the 14th Asian Symposium, APLAS 2016.
Azalea Raad has had two papers published in Programming Languages and System: Proceedings of the 14th Asian Symposium, APLAS 2016.
The papers are: [Verifying Concurrent Graph Algorithms](http://psvg.doc.ic.ac.uk/publications/Raad2016Verifying.html)(with Aquinas Hobor, Jules Villard and Philippa Gardner) and [DOM: Specification and Client Reasoning](http://psvg.doc.ic.ac.uk/publications/Raad2016DOM.html)(with José Fragoso Santos and Philippa Gardner)
The papers are: [Verifying Concurrent Graph Algorithms](http://psvg.doc.ic.ac.uk/publications/Raad2016Verifying.html)(with Aquinas Hobor, Jules Villard and Philippa Gardner) and [DOM: Specification and Client Reasoning](http://psvg.doc.ic.ac.uk/publications/Raad2016DOM.html)(with José Fragoso Santos and Philippa Gardner)
These and other group papers can be found on our [publications page](http://psvg.doc.ic.ac.uk/publications/)
These and other group papers can be found on our [publications page](http://psvg.doc.ic.ac.uk/publications/)
title:JSExplain discussed at ECMAScript standards committee meeting
---
Thomas Wood attended the latest [ECMAScript standards committee TC39](https://github.com/tc39/) meeting this November in San Francisco.
In previous meetings, we have presented a prototype of our JSExplain work to the committee and discussions with committee members at the latest meeting
furthered the design directions that JSExplain should take, to assist their needs with drafting revisions to the specification.
JSExplain is a reference interpreter derived from the JSCert project,
with a user interface designed to assist someone in their understanding of the workings of the ECMAScript language.
It is hoped that in the long run, the language the JSExplain specification is written in will closely match the English language of the specification.
Using it as an aid to drafting the specification will be the natural next step,
with the added advantage that the new features being proposed can be tested and experimented with interactively during their development.
It is envisaged that the JSExplain specification will be extractable for use in theorem provers to prove theories about the language, for example,
the soundness of the invariants [specified for Object internal methods](https://tc39.github.io/ecma262/2016/#sec-invariants-of-the-essential-internal-methods).
A [preliminary prototype version](https://jscert.github.io/jsexplain/branch/master/driver.html) of JSExplain is available, along with the [source code](https://github.com/jscert/jsexplain).
JSExplain is a collaboration with [Charguéraud](http://chargueraud.org/) and [Schmitt](http://people.rennes.inria.fr/Alan.Schmitt/) of [INRIA](http://www.inria.fr/).
Thomas has also agreed to assist with the [Regular Expression Lookbehind Assertions Proposal](https://github.com/littledan/es-regexp-lookbehind) targeted for the ES2017 specification.
