The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Thank you Tej and Pierre. Both the Electrolysis and Verasco works are relevant. We appreciate the pointers. The former, like CFML, requires semantics preservation. We can relax that constraint, which means we have a much easier problem to solve. We're very interested in Verasco as an example of the application of formally specified and verified analyses. If there's more, don't hesitate to let us know. At some point we'll update this thread with more details on what we're doing, once we've got it better written up. 

Thank you, Merci!

Kevin

On Mon, Jul 17, 2017 at 3:25 PM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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/