Introduction
When can we say that two programs are equivalent, in the sense that they exhibit the same observable behaviors? Or that one program refines another, in the sense that all observable behaviors of the first correspond to possible behaviors of the second? These questions arise in several areas of Software Science, ranging from software development methodologies—such as specification refinement—to verifying the correctness of compilers, as well as non-regression testing and the automatic correction of programming exercises. The concepts of equivalence and refinement between programs also play an important role in the theory of programming languages: since the most natural definition—namely, contextual equivalence—is particularly difficult to apply, many other approaches, which are less direct but more practical, have been studied. The course will provide an overview of this diversity of approaches and applications, with a particular focus on bisimulation techniques, logical relations, and relational logics.