Proving Soundness of Extensional Normal-Form Bisimilarities

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01650000
Contributor : Sergueï Lenglet <>
Submitted on : Tuesday, November 28, 2017 - 10:32:10 AM
Last modification on : Monday, October 7, 2019 - 5:50:50 PM

File

mfps.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

127

Files downloads

127