Proving Soundness of Extensional Normal-Form Bisimilarities
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 pro...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4041/pdf |
| _version_ | 1797268591377121280 |
|---|---|
| author | Dariusz Biernacki Serguei Lenglet Piotr Polesiuk |
| author_facet | Dariusz Biernacki Serguei Lenglet Piotr Polesiuk |
| author_sort | Dariusz Biernacki |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:55Z |
| format | Article |
| id | doaj.art-d6163e609ac845ed9189c1d88a46fb82 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:55Z |
| publishDate | 2019-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-d6163e609ac845ed9189c1d88a46fb822024-03-08T10:27:56ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-03-01Volume 15, Issue 110.23638/LMCS-15(1:31)20194041Proving Soundness of Extensional Normal-Form BisimilaritiesDariusz Biernackihttps://orcid.org/0000-0002-1477-4635Serguei LengletPiotr Polesiukhttps://orcid.org/0000-0002-7012-4346Normal-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.https://lmcs.episciences.org/4041/pdfcomputer science - logic in computer sciencecomputer science - programming languages |
| spellingShingle | Dariusz Biernacki Serguei Lenglet Piotr Polesiuk Proving Soundness of Extensional Normal-Form Bisimilarities Logical Methods in Computer Science computer science - logic in computer science computer science - programming languages |
| title | Proving Soundness of Extensional Normal-Form Bisimilarities |
| title_full | Proving Soundness of Extensional Normal-Form Bisimilarities |
| title_fullStr | Proving Soundness of Extensional Normal-Form Bisimilarities |
| title_full_unstemmed | Proving Soundness of Extensional Normal-Form Bisimilarities |
| title_short | Proving Soundness of Extensional Normal-Form Bisimilarities |
| title_sort | proving soundness of extensional normal form bisimilarities |
| topic | computer science - logic in computer science computer science - programming languages |
| url | https://lmcs.episciences.org/4041/pdf |
| work_keys_str_mv | AT dariuszbiernacki provingsoundnessofextensionalnormalformbisimilarities AT sergueilenglet provingsoundnessofextensionalnormalformbisimilarities AT piotrpolesiuk provingsoundnessofextensionalnormalformbisimilarities |