coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lifting programs into Coq

From: Kevin Sullivan <sullivan.kevinj AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Lifting programs into Coq
Date: Mon, 17 Jul 2017 15:58:44 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sullivan.kevinj AT gmail.com; spf=Pass smtp.mailfrom=sullivan.kevinj AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f182.google.com
Ironport-phdr: 9a23:a3qE8x+elCbWsf9uRHKM819IXTAuvvDOBiVQ1KB42uIcTK2v8tzYMVDF4r011RmSDNqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRx3miCkHOTA383zZhNJsg69Auh2tuwZyzpTIbI2JNvdzeL7Wc9MARWpGW8ZcTylPDZ2ib4sOCeoKIPtWr5T5p1sKrBu+GxOjBOXywTJPnX/2wKk60+AgEQHYxgMgGcgCsHfKo9XrNacSV+K1wbLHzTXGdfxW2DP95JLUfRAmpPGBRLR9etffx0koEgPKlFSQqYr9MjyJ1uQCqXKb7+V9Ve2xkW4osRxxrSW1yscrkInJiYQYwU3H+yVh2Is5O8G0RUphbdOnEJZcrTyWO5V1T884Xm1luzg2x7sbspChZicK0o4oxxvHZvyHbYeI5hXjWf6UIThihXJlfKuzhhio8US80+H8WNS43VVUoiZfndnMsXcN1xPX6seZUPdy4kCh2TOX2wDS7OFLP1w0mLLFJ5I9xrM8jJkevETZEiPrhkn7j7Waelgn9+S28+jnZ6/ppp6YN496kAH+NaEul9SkAeQlNggOW2mb+fqm273l50H5Q6tFjuM3kqnfspDXPssbpqujDA9U1oYv8QqwDzCj0NgAh3kIMEpFeA6bj4juI1zBPPf4De6mj1uwlDdr2uvJM6b6ApTNK3jDiK3ucax8605a0gozzMpQ64haCrEbc7rPXRq7v9vBSxQ9LgacwuD9Cdw72JlUETaEBbbcO6fPu3eJ4PguKq+CftlGliz6Lq0G6uDvizcChFsZfLeg29NDc228GvV4KkPfYnfyg9EDOWgPtws6CuftjQvRAnZoe3+uUvdktXkAA4W8ANKbSw==

Clément, Thank you. This is helpful. Per my response to an earlier response to my initial post, we're not looking to project the full semantics of the source language into Coq, but rather just enough to support the analysis at hand. You've solved a harder problem! We're happy to have this pointer. Thanks, again. --Kevin

On Mon, Jul 17, 2017 at 12:21 PM, Clément Pit-Claudel <cpitclaudel AT gmail.com> wrote:

On 2017-07-17 18:04, Kevin Sullivan wrote:
> Pointers to any relevant work would be much appreciated,

You may be interested in http://www.chargueraud.org/softs/cfml/

[Coq-Club] Lifting programs into Coq, Kevin Sullivan, 07/17/2017
- Re: [Coq-Club] Lifting programs into Coq, Adam Chlipala, 07/17/2017
  - Re: [Coq-Club] Lifting programs into Coq, Kevin Sullivan, 07/17/2017
- Re: [Coq-Club] Lifting programs into Coq, Clément Pit-Claudel, 07/17/2017
  - Re: [Coq-Club] Lifting programs into Coq, Tej Chajed, 07/17/2017
    - Re: [Coq-Club] Lifting programs into Coq, Pierre Courtieu, 07/17/2017
      - Re: [Coq-Club] Lifting programs into Coq, Kevin Sullivan, 07/17/2017
  - Re: [Coq-Club] Lifting programs into Coq, Kevin Sullivan, 07/17/2017
    - Re: [Coq-Club] Lifting programs into Coq, Clément Pit-Claudel, 07/17/2017