Simon Fowler ; Wen Kokke ; Ornela Dardha ; Sam Lindley ; J. Garrett Morris - Separating Sessions Smoothly

lmcs:9361 - Logical Methods in Computer Science, July 12, 2023, Volume 19, Issue 3 - https://doi.org/10.46298/lmcs-19(3:3)2023
Separating Sessions SmoothlyArticle

Authors: 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.


    Volume: Volume 19, Issue 3
    Published on: July 12, 2023
    Accepted on: April 13, 2023
    Submitted on: April 19, 2022
    Keywords: Computer Science - Programming Languages

    1 Document citing this article

    Consultation statistics

    This page has been seen 1049 times.
    This article's PDF has been downloaded 338 times.