This chapter is concerned with proving correctness of ADT implementations by exhibiting a simulation relation between a reference implementation (taken, or known, to be correct) and a candidate implementation (whose correctness is to be established).   The methodology generalizes Hoare's notion of abstraction functions to an arbitrary relation, and relies on Reynolds' notion of parametricity to conclude that related implementations engender the same observable behavior in all clients.