HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

A Complete Normal-Form Bisimilarity for State

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 Stovring 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.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Thursday, January 31, 2019 - 2:56:52 PM
Last modification on : Wednesday, November 3, 2021 - 7:09:19 AM
Long-term archiving on: : Wednesday, May 1, 2019 - 7:25:00 PM


Files produced by the author(s)


  • HAL Id : hal-02002115, version 1


Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. A Complete Normal-Form Bisimilarity for State. [Research Report] RR-9251, Inria Nancy - Grand Est. 2019. ⟨hal-02002115⟩



Record views


Files downloads