Skip to Content.
Sympa Menu

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

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




Archive powered by MHonArc 2.6.18.

Top of Page