Leroy uses simulation relations as a means of showing compiler correctness; the basic idea is that a simulation relation is an asymmetric binary relation between states in two different small step semantics such that initial states are related, and the relation is preserved under a single step in the first semantics by a finite sequence of steps (or sometimes none) in the second. This can be augmented with notions of trace inclusion, and then determinism proofs allow trace equivalence to be shown from the existence of a simulation.
Chlipala covers this in his text (which is where I first learned about it), but there are no citations, and I'm not sure whether the method is due to Leroy or if it has earlier origins.