Formalizing the meta-theory of program equivalences in Coq

• The paper
• The code
• The slides of the ICTCS talk