coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lifting programs into Coq

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Lifting programs into Coq
Date: Mon, 17 Jul 2017 19:25:37 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f174.google.com
Ironport-phdr: 9a23:mBKpMxPGlPtXqqzj1C0l6mtUPXoX/o7sNwtQ0KIMzox0Iv76rarrMEGX3/hxlliBBdydsKMbzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgIOT428mHZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoakYoUVDuoOI/xYr5PjqFATsxa+AhSsBPnzyj9JmHD2wLAx3uM5EQHHwgMgBcgOv2rOoNrpM6cSTPq1zLXJzTrdcvNbwjj96I3SfRAgpfGAR65/cc3UyUQ2EQ7Ok1ueqYvgPzyP1+QNtXCW4PZgVe21kW4npBxxrSa1xsg2l4nGm5gZylfe9SV22Io1JNu4SFR6YdG+CpdQuTuaO5N5QsMjX2FouDs6xaYctZGneygKzZIqzAPcZfyfa4WE/A7vWeKLLTp7hH9pYq+ziwix/ES61+HxVMa53VBXpSRfiNbMrGoC1xnL58iHVPR9+kCh1C6K1w/J6+FEJVk4lKTBK5I927IwmIcfvEbMEyPsl0X2i6iWdkog+ue28ejofrLmppqEO491jAHxLLgul9ShDegkNgUCRWuW9OSm2LH+40H0Q69GguA0n6TWqJzaIN4Upq+9Aw9byIYj7BO/Ai++0NQZg3YHNkhFdwydg4f1PFHOPer4Deu+g1uyjTdm3P/GPrj7DZXMKnjPiqvufbF460JE0go80chf545ICrEGOP/8RkjxtMXBAhAlNwy03v3oBc5m1oIeXGKPGrWWPLnTsV+O/OIvIvODaJUbuDbneLAZ4KvlimZ8klsAd4Go24EWYTa2BKdIOUKcNELtj80bHC8huRckUO3nlRXWST9efWy/Gak7+ysnCY+7JYjGT4GpxreG2XHoTdVtemlaBwXUQj/TfIKeVqJUZQ==

I think compcert is exactly what you ask for for C programs. And you can look at Verasco for a proved analyzer.

http://compcert.inria.fr/

http://compcert.inria.fr/verasco/

Pierrr

Le lun. 17 juil. 2017 à 19:02, Tej Chajed <tchajed AT mit.edu> a écrit :

While it does not involve Coq, you might also take a look at Sebastian Ulrich's master's thesis: https://github.com/Kha/electrolysis, which converts Rust programs to Lean for verification.

On Mon, Jul 17, 2017 at 5: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