Proving Soundness of Extensional Normal-Form Bisimilarities
2019
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.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
0
Citations
NaN
KQI