[Coq-Club] Is there a minimal subset of JavaScript, both useful for formal verification and practical enough?

[Ilmārs Cīrulis]

What's your opinions (or suggestions to read etc.) about this topic?

Thanks in advance,
Ilmārs Cīrulis

[Greg Morrisett]

Two key projects to consider (there are probably others):

* http://www.jswebtools.org/ --- Shriram Krishnamurthy's work; nice
core language that the full language can be compiled into.
* http://psvg.doc.ic.ac.uk/research/javascript.html --- Philippa Gardner's
work; nice formalization in Coq;

-Greg

Post by Ilmārs Cīrulis
What's your opinions (or suggestions to read etc.) about this topic?
Thanks in advance,
Ilmārs Cīrulis

[Alan Schmitt]

Hello,

* http://www.jswebtools.org/ --- Shriram Krishnamurthy's work; nice core
language that the full language can be compiled into.
* http://psvg.doc.ic.ac.uk/research/javascript.html --- Philippa Gardner's work;
nice formalization in Coq;

There is a link between the two, which is still work in progress:
https://github.com/tilk/LambdaCert

Best,

Alan

[Ilmārs Cīrulis]

Big thank you!

Ilmars

On Fri, May 13, 2016 at 10:10 AM, Alan Schmitt <

Post by Alan Schmitt
Hello,

* http://www.jswebtools.org/ --- Shriram Krishnamurthy's work; nice core
language that the full language can be compiled into.
* http://psvg.doc.ic.ac.uk/research/javascript.html --- Philippa

Gardner's work;

nice formalization in Coq;

https://github.com/tilk/LambdaCert
Best,
Alan
--
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2015-04: 403.26, 2016-04: 407.42