Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Lifting programs into Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lifting programs into Coq


Chronological Thread 
  • 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 16:14:23 -0400
  • Authentication-results: mail3-smtp-sop.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-wm0-f46.google.com
  • Ironport-phdr: 9a23:Bq0oBh33PrW+w2umsmDT+DRfVm0co7zxezQtwd8ZseIUIvad9pjvdHbS+e9qxAeQG96KtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLniikHOT43/m/Ul8J+kr5UrQm7qBBj2YPZep2ZOOZ8c67bYNgURXBBXsFUVyFZB42zcZUPD+sHPe1Fsof9ul8OrR+/BQmyHuzvzCJDi3jt3a0n1+QhFQDG3BI6ENIIqnjUr8v6NLkTUeCzzqnF1jrDb/ZM1jf87IjEaAwuofaJXb9pd8fa1EchFwTAjlqKqIzlOSuY2fgNs2eB9epgWv+vhHA9qw5rvzig290gio7ThoIa0lzE9CN5wJw0JdKiUkJ7b8SkHINftyGbK4t2Qt4iTHpytCkmzb0GvJi2dzUJxpQ/3xPSafOKf5KV7h79VOudOzR1iGx/dL+whhu/91WrxPfmWcmuyllKqzJIktnSuXAJ0Bze8s2HReF8/kelwDqO2QXT5v1dLUA6mqfWKoQtwrE3lpoUvkTDGjH5lF/qg6+Rc0Uo4umo6+L5bbX6vpKRNYB5hhvjPqgwmsGzG+c1PhYUU2WU+OmwzLjj8lf4QLVOgP02iK7ZsJXCKMQAu665BwtV0oc96xmlCTeqytcYkmcZLFJEfhKHjZPkO17LIP/iDPe/h06gnytsx/DDJrHhGInCLmDfkLf9erZw81JTyA0qzdxG+51UDqwBL+noV0/qtN3YCwc5PBauz+bmDtV9zIIeVniVDq+XKqOB+WOPs6gkJPDJb4sIsh78LeIk7rjglzVxzVQaZOyi2YYdQHG+BPVvZUuDNynCmNAEREQHoAs4BNf3jFmDTzdVLyKpQqY45y8yDsSlAJnCQIKFj7mI3SP9FZpTMDMVQmuQGGvlIt3XE8wHbzifd5ds

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.


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/





Archive powered by MHonArc 2.6.18.

Top of Page