A Complete Normal-Form Bisimilarity for State
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk · Lecture notes in computer science · 2019
Abstract We present a sound and complete bisimilarity for an untyped $$\lambda $$ -calculus with higher-order local references. Our relation compares values by applying them to a fresh variable, like normal-form bisimilarity, and it uses environments to account for the evolving store. We achieve completeness by a careful treatment of evaluation contexts comprising open stuck terms. This work improves over Støvring and Lassen’s incomplete environment-based normal-form bisimilarity for the $$\lambda \rho $$ -calculus, and confirms, in relatively elementary terms, Jaber and Tabareau’s result, that the state construct is discriminative enough to be characterized with a bisimilarity without any quantification over testing arguments.