I have came accross an article that have not been mentioned here. There is apprently an effort for formalizing LLVM IR in Coq that is partially based on CompCert effort.
"Formalizing the LLVM Intermediate Representation for Verified Program Transformations". http://www.cis.upenn.edu/~santoshn/popl12_vellvm.pdf Regards, Constantine
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
