Relational reasoning plays an important role in programming languages. For example, it is used to show that optimized versions of data structures behave the same as their non-optimized versions (contextual equivalence), to prove linearizability of concurrent data structures (contextual refinement), to prove correctness of program transformations (contextual refinement), and to prove that varying secret information does not lead to different behavior that can be observed by attackers (non-interference). In this talk, I will describe recent developments in concurrent separation logic (in the context of the Iris framework in the Coq proof assistant) that enable modular and mechanized relation reasoning in the context of rich languages with higher-order state and fine-grained concurrency.