Name
Abstract | ||
|---|---|---|
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 a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.4230/LIPIcs.CONCUR.2021.36 | CONCUR |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Simon Fowler | 1 | 2 | 1.40 |
| Wen Kokke | 2 | 0 | 1.35 |
| Ornela Dardha | 3 | 0 | 2.03 |
| Sam Lindley | 4 | 24 | 3.46 |
| J. Garrett Morris | 5 | 6 | 0.76 |