Introduction
This year, Xavier Leroy’s course will focus on the problem of program equivalence: how can we establish that two programs behave identically or are compatible? This question arises in several fields, ranging from compiler verification to nonregression testing and the automatic correction of programming exercises, and plays an important role in the formal semantics of programming languages.