Authors: Simon Fowler ; Wen Kokke ; Ornela Dardha ; Sam Lindley ; J. Garrett Morris
NULL##NULL##NULL##NULL##NULL
Simon Fowler;Wen Kokke;Ornela Dardha;Sam Lindley;J. Garrett Morris
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.
Session Types for Reliable Distributed Systems (STARDUST); Funder: UK Research and Innovation; Code: EP/T014628/1
Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233
A programming language bridging theory and practice for scientific data curation; Funder: European Commission; Code: 682315
CAREER: Extensibility in Theory and Practice; Funder: National Science Foundation; Code: 2044815
Effect Handler Oriented Programming; Funder: National Science Foundation; Code: MR/T043830/1
From Data Types to Session Types---A Basis for Concurrency and Distribution; Funder: UK Research and Innovation; Code: EP/K034413/1
Bibliographic References
1 Document citing this article
Simon Fowler;Duncan Paul Attard;Franciszek Sowul;Simon J. Gay;Phil Trinder, 2023, Special Delivery: Programming with Mailbox Types, Proceedings of the ACM on Programming Languages, 7, ICFP, pp. 78-107, 10.1145/3607832, https://doi.org/10.1145/3607832.