A Mechanized Bisimulation for the Nu-Calculus

We introduce a Sumii-Pierce-Koutavas-Wand-style bisimulation for Pitts and Stark’s nu-calculus, a simply-typed lambda calculus with fresh name generation. This bisimulation implies contextual equivalence and provides a usable and elementary method for establishing all the subtle equivalences given by Stark. We also describe the formalization of the metatheory and of the examples in the Coq proof assistant.