coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lifting programs into Coq

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Lifting programs into Coq
Date: Mon, 17 Jul 2017 12:07:18 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:0tQImxG4+vJJT5dRVNufx51GYnF86YWxBRYc798ds5kLTJ78pcuwAkXT6L1XgUPTWs2DsrQf2rWQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDiwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSMn/mHZisJ+j6xVrxyuqBN934HZe5uaOOZkc67HYd8XS2hMU8BMXCJBGIO8aI4PAvIdMOlFtYb9okYFoAW+BQmoBePv0iVHhnvs0qYn1OkuCxzJ0xYlH90Sq3nbsM71O70TUeCx1qXIyDTDb+9M1Tjj9YfIbwksrPeRVrxzacrc0VQjGx3Gg1mKp4HpIymZ2voXv2SF8uZsSfqjh3M5pwxyuDSiyNsghpPNi44L0FzI6zt1zJszKNalUkB0e8SkH4FVtyyCN4t5XMciQ2ZwtSY9170GpZG7fC8LyJQhyB7TcueHc5SS7RL/TumdOyt3hGl/d7K+gxa+602gyuzgVsWuzllFszdFnsHNtnALyRPT9tCKRuZj8kqiwzqC2Rzf5vtaLUwui6bXNoItzqY1lpUJsETDGiH2mF/xjK+Tbkgr4PWn5P7iYrr6vZKTK5R0hRv/MqQqgMC/BOU4MhQUU2eF5Ou8yaXv/VflT7VSkv02jq7ZvYjGKsQcv661GhNa0oI+6xmkFDqmy9QZnXwfLF1fYh6Hjo7pO0vPIP/iF/u/jU6sw39XwKXNOaSkCZHQJFDClq3gdPBz8R1y0g02mPlT7pccIbEFIer6Xka54NXUBxoyGwevyufjTtB8ysUTVX/ZUfzRC7/brVLdvrFnGOKLfoJA4Ds=

Can you clarify your objective a bit more? Imp probably isn't expressive enough to encode Java or C fully, without implementing an explicit interpreter/runtime for those languages in Imp. It doesn't sound practical to use a "toy" educational language for modeling industrial-scale languages.

On 07/17/2017 12:04 PM, Kevin Sullivan wrote:

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