A Complete Normal-Form Bisimilarity for State - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

A Complete Normal-Form Bisimilarity for State

Résumé

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.
Fichier principal
Vignette du fichier
final.pdf (333.02 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02086532 , version 1 (01-04-2019)

Identifiants

Citer

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⟩
129 Consultations
70 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More