The Coq mailing list

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

Thank you. We're exploring a case where we don't need a language rich enough easily to implement arbitrary Java, C, or other programs. Our lifting operations are partial: sufficient for the analysis at hand.

--Kevin

On Mon, Jul 17, 2017 at 12:07 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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