coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Is there a minimal subset of JavaScript, both useful for formal verification and practical enough?
Chronological Thread
- From: Greg Morrisett <morrisett AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Is there a minimal subset of JavaScript, both useful for formal verification and practical enough?
- Date: Thu, 12 May 2016 09:39:32 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=morrisett AT gmail.com; spf=Pass smtp.mailfrom=morrisett AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f42.google.com
- Ironport-phdr: 9a23:95LqUhPwq23aDnZrvgAl6mtUPXoX/o7sNwtQ0KIMzox0KP/8rarrMEGX3/hxlliBBdydsKIVzbOH+P69EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35XxjrH5pcCbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7ayWERXS0zlQBSAhPI8A2yCpL2qDH7redhxAGVOMT3SfY/XjH0vPQjcwPhlCpSb21xy2rQkMEl1K8=
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
On Thu, May 12, 2016 at 9:23 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:
What's your opinions (or suggestions to read etc.) about this topic?Thanks in advance,Ilmārs Cīrulis
- [Coq-Club] Is there a minimal subset of JavaScript, both useful for formal verification and practical enough?, Ilmārs Cīrulis, 05/12/2016
- Re: [Coq-Club] Is there a minimal subset of JavaScript, both useful for formal verification and practical enough?, Greg Morrisett, 05/12/2016
Archive powered by MHonArc 2.6.18.