Autor: |
Fowler, Simon, Kokke, Wen, Dardha, Ornela, Lindley, Sam, Morris, J. Garrett |
Rok vydání: |
2021 |
Předmět: |
|
Zdroj: |
Logical Methods in Computer Science, Volume 19, Issue 3 (July 12, 2023) lmcs:9361 |
Druh dokumentu: |
Working Paper |
DOI: |
10.46298/lmcs-19(3:3)2023 |
Popis: |
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. |
Databáze: |
arXiv |
Externí odkaz: |
|