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: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <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: Mon, 16 May 2016 12:11:29 +0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f170.google.com
Ironport-phdr: 9a23:lA1YHRyW78JVEnHXCy+O+j09IxM/srCxBDY+r6Qd0ewSIJqq85mqBkHD//Il1AaPBtWKragawLOO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt+U1Zr8jrj60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mooRLVry/dKAlR5RZCi4nOiY7/oej4RLEVE6E4mYWemQQiBtBRQbfukLURJD05wr+s0Fnw2GxPNfrSbEvEWCj66JiUgSugyYdKjo460nYj8VxiORQpxf39E83+JLdfIzAbKk2RajaZ95PHWc=

Big thank you!

Ilmars

On Fri, May 13, 2016 at 10:10 AM, Alan Schmitt <alan.schmitt AT polytechnique.org> wrote:

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

[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