coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lifting programs into Coq

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Lifting programs into Coq
Date: Mon, 17 Jul 2017 18:00:41 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-1.mit.edu
Ironport-phdr: 9a23:ePTdAhVXdIvOP/cGiDykJxPLRg/V8LGtZVwlr6E/grcLSJyIuqrYYxKAt8tkgFKBZ4jH8fUM07OQ6PG/HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLdwIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7VhMx+jKxVrhG8qRJh34HZe5uaOOZkc67HYd8WWWhMU8BMXCJBGIO8aI4PAvIfM+lGrYn2ukUDrRukCgmuGuzg1yJDi3jq3aIm0+QuCwPG0xI9EN8VtXTUrcn1OL0MXu+o0anF1DPOZO5Y1zf67YjHaBEhofeUUL1sccre01MvFwzYjlqOs4zqJS6V2fkXv2ic9epgWvqji2EmqwFtojiv29wjhpPViYISz1DJ8zhyzoUtJdCgVUJ2YsSoHZ9Kuy2EN4Z6WN4uT39wtCs4xbAKo4O3cDYKxZg9xBPTdeaLfoeM7x/lSe2fOy13hGh/d7K6nxuy8Vavyun7VsSszVlKqytEnsDJtn8X1hzT7tOHReVh8Uu4wjaAyxrc6udCIU8qj6rXMoMtzqQ1lpoSrUTPBDH5l1jrjKOOd0Uk/Pan6/j/b7n7pZKQLYt5hhvgPqkugMCzHPo0PhALX2eB+OS80LPj/Vf+QLVPlvA2jrXWsJDAKsQZuKG2HhRY0oMi6xajFTupzskXnWQfIFJfZB2Hl5TpO03JIP3gEfi/hE2snC53yPDCI73uGY7ALmPDkbfkZbZy8VRQyAs1zdBF5pJbEKsNIPzpWhy5iNuNBRggdgew3uyvXN56z8YVXX+FKq6fKqLb91GSsLEBOe6JMbMYun7WK/En6vKm2WMymVYfcKWB2JoLLn20A6I1cA2ifXPwj4JZQi8xtQ0kQbmyhQ==

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