GitHub repository: Biebar/imm
Primary language: Coq
Description: Intermediate Memory Model (IMM) and compilation correctness proofs for it