Conference proceeding
Separating Sessions Smoothly
08/13/2021
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.
Details
- Title: Subtitle
- Separating Sessions Smoothly
- Creators
- Simon FowlerWen KokkeOrnela DardhaSam LindleyJ. Garrett Morris
- Resource Type
- Conference proceeding
- Language
- English
- Date published
- 08/13/2021
- Academic Unit
- Computer Science
- Record Identifier
- 9984259434602771
Metrics
3 Record Views