SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Wed 20 Oct 2021 10:50 - 11:05 at Zurich D - Functional Programming Chair(s): Nada Amin
Wed 20 Oct 2021 18:50 - 19:05 at Zurich D - Functional Programming - Mirror Chair(s): Atsushi Igarashi

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
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