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
Journal articles

Proving Soundness of Extensional Normal-Form Bisimilarities

Abstract : Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in lambda-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows 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 eta-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 up to context technique are sound. We illustrate our technique with three calculi: the call-by-value lambda-calculus, the call-by-value lambda-calculus with the delimited-control operators shift and reset, and the call-by-value lambda-calculus with the abortive control operators call/cc and abort. In the first two cases, there was previously no sound up to context technique validating the eta-law, whereas no theory of normal-form bisimulations for a calculus with call/cc and abort has been presented before. Our results have been fully formalized in the Coq proof assistant.
Document type :
Journal articles
Complete list of metadata

Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Monday, April 1, 2019 - 1:55:33 PM
Last modification on : Tuesday, January 25, 2022 - 11:44:06 AM

Links full text




Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Proving Soundness of Extensional Normal-Form Bisimilarities. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019, 15 (1), pp.31:1-31:24. ⟨10.23638/LMCS-15(1:31)2019⟩. ⟨hal-02086527⟩



Record views