In this paper we present a novel simulation relation for
proving correctness of program transformations that combines
syntactic simulations and logical relations. In particular, we
establish a new kind of simulation diagram that uses a
small-step or big-step semantics in the source language and an
untyped, step-indexed logical relation in the target language.
Our technique provides a practical solution for proving
semantics preservation for transformations that do not preserve
reductions in the source language. This is common when
transformations generate new binder names, and hence
$\alpha$-conversion must be explicitly accounted for, or when
transformations introduce administrative redexes. Our
technique does not require reductions in the source language to
correspond directly to reductions in the target
language. Instead, we enforce a weaker notion of semantic
preorder, which suffices to show that semantics are preserved
for both whole-program and separate compilation. Because our
logical relation is transitive, we can transition between
intermediate program states in a small-step fashion and hence
the shape of the proof resembles that of a simple small-step
simulation.

We use this technique to revisit the semantic correctness of a
continuation-passing style (CPS) transformation and we
demonstrate how it allows us to overcome well-known
complications of this proof related to $\alpha$-conversion and
administrative reductions. In addition, by using a logical
relation that is indexed by invariants that relate the resource
consumption of two programs, we are able show that the
transformation preserves diverging behaviors and that our CPS
transformation asymptotically preserves the running time of the
source program. Our results are formalized in the Coq proof
assistant. Our continuation-passing style transformation is
part of the CertiCoq compiler for Gallina, the specification
language of Coq.