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?

From: Alan Schmitt <alan.schmitt AT polytechnique.org>
To: Greg Morrisett <morrisett AT gmail.com>
Cc: 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: Fri, 13 May 2016 09:10:07 +0200

Hello,

On 2016-05-12 15:39, Greg Morrisett
<morrisett AT gmail.com>
writes:

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

There is a link between the two, which is still work in progress:
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

Attachment: signature.asc
Description: PGP signature

[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
  - Re: [Coq-Club] Is there a minimal subset of JavaScript, both useful for formal verification and practical enough?, Alan Schmitt, 05/13/2016
    - Re: [Coq-Club] Is there a minimal subset of JavaScript, both useful for formal verification and practical enough?, Ilmārs Cīrulis, 05/16/2016