It's a semantics for the intermediate representation used by most of the LLVM optimization passes defined in a theorem prover. With it you can, for example, wr

It's a semantics for the intermediate representation used by most of the LLVM optimization passes defined in a theorem prover. With it you can, for example, write your own LLVM pass in Coq's specification language and prove that it can't introduce bugs by changing the meaning of a program. See also Compcert[1] and CakeML[2] for some other recent work in this area. [1] http://compcert.inria.fr/ http://compcert.inria.fr/ [2] https://cakeml.org/ https://cakeml.org/