The Coq mailing list

[Chan Ngo <chan.ngo2203 AT gmail.com>]

Dear all,

Thanks for the references. The Herms’ thesis is exactly what I wanted to point out in the previous emails.

This thread becomes interesting as on my side :-) By the way, I would like to turn the subject a little bit but in the same track. We consider the LLVM compiler, I assume that its core implementation is formally proved (e.g., some work based on translation validation for proving the correctness of the compiler’s transformations and optimizations). Now, assume that I want to develop a new “pass” (an optimization - in C++ and uses the data structures and API functions provided by LLVM) for  LLVM and I want to make sure that my pass implementation is formally proved. I end up with two methods below:

M1.

- Develop a translation module that translates my code in C++ to Gallina (I think it is not easy task)

- Prove the correctness of this module

- Prove the correctness of the pass implementation based on the translated Gallina in Coq (i.e., based on the tool like VST)

M2.

- Specify the pass implementation in Coq, meaning that somehow we define a programming language with constructors coming from the data structures and API functions in LLVM (i.e., the concept of Basic Block, Functions, Modules in LLVM IR)

- Prove the correctness of the pass based on the above specification in Coq (i.e., based on the tool like VST)

- Automatically generated the C++ code of the pass from Coq

How do you think about pros and cons of each methods?

Thanks,

---

Chan Ngo

INRIA,

(+33)02 99 84 72 84

chan.ngo AT inria.fr

http://people.rennes.inria.fr/Chan.Ngo