In the last several years, a number of effective methods have been developed for reasoning about program equivalence in higher-order imperative languages like ML. Most recently, we proposed parametric bisimulations (PBs), which fruitfully synthesize the direct coinductive style of bisimulations with the flexible invariants on local state afforded by Kripke logical relations, and which furthermore support transitive composition of equivalence proofs. However, the PB model of our previous work suffered from two limitations. First, it failed to validate the eta law for function values, which is important for our intended application of compiler certification. Second, it was not clear how to scale the method to reason about control effects.
In this paper, we propose stuttering parametric bisimulations (SPBs), a variant of PBs that addresses their aforementioned limitations. Interestingly, despite the fact that the eta law and control effects seem like unrelated issues, our solutions to both problems hinge on the same technical device, namely the use of a "logical" reduction semantics that permits finite but unbounded stuttering in between physical steps. This technique is closely related to the key idea in well-founded and stuttering bisimulations, adapted here for the first time to reasoning about open, higher-order programs. We present SPBs---along with meta-theoretic results and example applications---for a language with recursive types and first-class continuations. Following our previous account of PBs, it is straightforward to extend SPBs to handle abstract types and general mutable references as well (see the appendix for details). All our results have been fully mechanized in Coq.