<div dir="ltr"><div>I am interested in type-based verification of LLVM IR in the areas of certified compilation and software verification. It seems to me that the LLVM IR type system is rather informal in the sense that there is no paper with a proper formalization of the type rules, and for example, a proof of soundness for well-formedness of the code. </div>
<div>I would like to know if you are aware of any work in this direction for LLVM IR so that I can compare with my own implementation.</div><div>Moreover, it would be valuable to get some feedback on suitable type-based analysis that the LLVM community would like to have in the infrastructure.</div>
<div><br></div><div>Regards,</div><div>Marcelo</div></div>