coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Lifting programs into Coq
Date: Mon, 17 Jul 2017 12:04:01 -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-f179.google.com
Ironport-phdr: 9a23:pOyNah3CDaeYrBGDsmDT+DRfVm0co7zxezQtwd8Zse0SLPad9pjvdHbS+e9qxAeQG96KtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiCkJOT0k/m/JlsN9l7hUrA67qhFl34LYfIOYOfxjda3dZ9MaQm9BU95UWSNfHIO8bo0PBPccM+ZFq4n9o1oOrQWkCgmqGejizSRIhmLy3a0+0uQhDxvJ3Ao6E9INrnvUstT1NKEQUe2uw6nIyC/Mb/JS2Tvn9IfIdRUhrOiKULltcsTR0VEiGx3ZgliUs4DoPDOY2v4Qv2SF7OdsT/+jhmwjpgx3vzOh3N0jipPTiYIQ0l3E9Tt2wIIyJdCgTU50e9+kEJ9JuyCULYt6XtouQ291tCs4zrAKo5G7fC8NyJQowx7QdeaLfJSP4hLmTOqRIDF4i2x5eL+nmRq+7Uytxvf/W8S0ylpGszRJn9rWunwQ1RHe7tCLSv5n8Ueg3TaP2RrT6uZBIU0sjqrbNpohwroxlpoNq0vDGDX6mEbog6+Id0Uk/Oqo5v/oYrXjvJCcNot0hhviPaQpn8yzGf44PRQWX2iH5eS806Xu8lH+QLVTl/E5jq3ZsI3BKskAva64AwpV0p455BqlDjem1s4YnXgdI15fdhKHlduhB1abavv/FLK0h0mmuDZt3fHPeLP7SN2ZJX/a1bzlYLxV6khGyQN1w8oJtLxODbRUA//tW0m5j8HcCh4nOgr8l/36DNF8yIoYH2GCHK6fMovdtFaJ4qQkJOzaN9xdgyr0N/Vwv62mtnQ+g1JIJaQ=

Dear Colleagues:

I'm looking for pointers to related work.

We know that one can embed arbitrary languages in Coq and then reason about programs in those languages using the machinery of Coq.

What I don't know about -- and here's where I seek pointers -- are approaches that lift/map programs in languages such as Java and C into corresponding programs in languages such as Pierce's Imp, in order to perform analyses specified and certified in Coq on such programs.

Pointers to any relevant work would be much appreciated,

Kevin Sullivan

University of Virginia

[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