Proving Soundness of Extensional Normal-Form Bisimilarities - Archive ouverte HAL Access content directly
Conference Papers Year :

Proving Soundness of Extensional Normal-Form Bisimilarities

(1) , (2) , (1)


Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in λ-calculi by decomposing their normal forms into bisimilar subterms. Besides, they allow for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of η-expansion and usually relies on ad-hoc proof methods which depend on the language. In this paper, we propose a more systematic proof method to show that an extensional normal-form bisimilarity along with its corresponding bisimulation up to context are sound. We illustrate our technique with the call-by-value λ-calculus, before applying it to a call-by-value λ-calculus with the delimited-control operators shift and reset. In both cases, there was previously no sound bisimulation up to context validating the η-law. Our results have been formalized in the Coq proof assistant.
Fichier principal
Vignette du fichier
mfps.pdf (351.65 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01650000 , version 1 (28-11-2017)



Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Proving Soundness of Extensional Normal-Form Bisimilarities. Mathematical Foundations of Programming Semantics XXXIII, Jun 2017, Ljubljana, Slovenia. ⟨10.1016/j.entcs.2018.03.015⟩. ⟨hal-01650000⟩
104 View
128 Download



Gmail Facebook Twitter LinkedIn More