Separating Sessions Smoothly
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2021
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909103578677248 |
|---|---|
| author | Fowler, Simon Kokke, Wen Dardha, Ornela Lindley, Sam Morris, J. Garrett |
| author_facet | Fowler, Simon Kokke, Wen Dardha, Ornela Lindley, Sam Morris, J. Garrett |
| contents | This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain an operational correspondence between HGV and HCP -- a process calculus based on hypersequents and in a propositions-as-types correspondence with classical linear logic (CLL). Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard's Mix rule, a crucial ingredient for channel forwarding and exceptions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2105_08996 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Separating Sessions Smoothly Fowler, Simon Kokke, Wen Dardha, Ornela Lindley, Sam Morris, J. Garrett Programming Languages This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain an operational correspondence between HGV and HCP -- a process calculus based on hypersequents and in a propositions-as-types correspondence with classical linear logic (CLL). Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard's Mix rule, a crucial ingredient for channel forwarding and exceptions. |
| title | Separating Sessions Smoothly |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2105.08996 |