Contextual refinement is a formalisation of an asymmetric comparison between program fragments. It asserts that the observable result of a program fragment can be reproduced by another program fragment in an arbitrary context. Compiler optimisation, for example, can be validated by proving contextual refinement.

One existing approach to proving contextual refinement is to use Abramsky’s applicative bisimilarity. After constructing an applicative bisimulation, one needs to prove that the applicative bisimulation is a congruence, which means that the applicative bisimulation is preserved by language constructs. The proof of congruence typically uses Howe’s method.

We propose yet another approach that uses a simulation notion. This approach reverses the two steps of Abramsky’s approach. Namely, one first constructs a relation that is closed under language constructs, and then prove that the relation is a simulation. Consequently, this approach does not need Howe’s method.

In this talk we explain how we are “climbing up a ladder” of advanced features using the new approach: namely, divergence, state, nondeterminism, I/O, and probability. The first steps on the ladder accommodates only divergence. We introduced a notion of counting simulation, and showed that graphical local reasoning can be used to establish contextual refinement. The next step on the ladder was to generalise the notion of counting simulation to accommodate nondeterminism and I/O, introducing a generalised simulation notion dubbed preoder-constrained simulation. Finally, we refined the first steps using term-rewriting techniques. We observed that the notion of counting simulation has a striking similarity with the notion of local coherence that can be found in the term-rewriting literature. By developing critical pair analysis for local coherence, we managed partial automation of contextual refinement proofs.