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 <>
Submitted on : Monday, April 1, 2019 - 1:55:33 PM
Last modification on : Saturday, November 21, 2020 - 9:54:03 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