| Autor: |
Biernacki, Dariusz, Lenglet, Serguei, Polesiuk, Piotr |
| Rok vydání: |
2017 |
| Předmět: |
|
| Zdroj: |
Logical Methods in Computer Science, Volume 15, Issue 1 (March 29, 2019) lmcs:4041 |
| Druh dokumentu: |
Working Paper |
| DOI: |
10.23638/LMCS-15(1:31)2019 |
| Popis: |
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. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
