Title: Program equivalence and compositional compiler correctness Abstract: We introduce a notion of program equivalence between different languages and talk about what kind of mathematical techniques are used, how it gives a compositional notion of compiler correctness and more ambitiously how it may be seen as a technique to prove the correctness of programs. We also briefly discuss how these ideas can be formalized and verified in the formal proof assistant Coq.