# A Complete Normal-Form Bisimilarity for State

2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : We 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.
Document type :
Conference papers

Cited literature [19 references]

https://hal.inria.fr/hal-02086532
Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Monday, April 1, 2019 - 1:59:36 PM
Last modification on : Wednesday, November 3, 2021 - 7:57:44 AM
Long-term archiving on: : Tuesday, July 2, 2019 - 1:54:53 PM

### File

final.pdf
Files produced by the author(s)

### Citation

Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. A Complete Normal-Form Bisimilarity for State. FoSSaCS, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17127-8_6⟩. ⟨hal-02086532⟩

Record views