A Complete Normal-Form Bisimilarity for State

International audienceWe present a sound and complete bisimilarity for an untyped $λ-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 $λρ-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