coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] transforming imperative language into Coq specification

From: Stéphane Glondu <steph AT glondu.net>
To: geng chen <chengeng4001 AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] transforming imperative language into Coq specification
Date: Tue, 01 Dec 2009 23:16:10 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Openpgp: id=49881AD3

geng chen a écrit :
> Recently, I am working on transforming the C and assembly code into Coq
> code(Gallina).
> I will be happy if you can send some codes, papers or other kinds of
> materials
> for transforming the C and assembly code into Coq code or the
> implementation of
> C or other imperative language semantics in Coq.

You might be interested by:

Magnus O. Myreen and Michael J. C. Gordon. Transforming Programs into
Recursive Functions. In the Brazilian Symposium on Formal Methods
(SBMF), 2008.
http://www.cl.cam.ac.uk/%7Emom22/transforming.pdf

Cheers,

--
Stéphane

Re: [Coq-Club] transforming imperative language into Coq specification, Stéphane Glondu