LIVE

Correction of LLVM

Goal

Links

  • Blog post of Lindsey Kuper : request of an abstract and proven language on top of LLVM
  • LLVM M.D. : a Haskell validator of LLVM code transformations
  • Beginning of a PhD to formalize the LLVM's semantics in Coq