Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence
Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos · 2024
We propose Pushdown Normal Form (PDNF) Bisimulation to verify contextual equivalence in higher-order functional programming languages with local state. Similar to previous work on Normal Form (NF) bisimulation, PDNF Bisimulation is sound and complete with respect to contextual equivalence. However, unlike traditional NF Bisimulation, PDNF Bisimulation is also decidable for a class of program terms that can reach configurations of unbounded size, so long as the source of unboundedness is the call stack. Our approach relies on the principle that, in model-checking for reachability, pushdown systems can be simulated by finite-state automata designed to accept their initial/final stack content. We embody this in a stack-less Labelled Transition System (LTS), together with an on-the-fly saturation procedure for call stacks, upon which bisimulation is defined. We develop up-to techniques and a prototype implementation able to verify equivalences from the literature and others inspired by real code, which were out of reach for previous work.