Wen Kokke ; Ornela Dardha - Prioritise the Best Variation

lmcs:8867 - Logical Methods in Computer Science, December 18, 2023, Volume 19, Issue 4 - https://doi.org/10.46298/lmcs-19(4:28)2023
Prioritise the Best VariationArticle

Authors: Wen Kokke ; Ornela Dardha

    Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical Processes (CP)$-$a process calculus based on classical linear logic$-$deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (GV)$-$a linear concurrent $\lambda$-calculus$-$deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork. In both CP and GV, deadlock freedom is achieved at the expense of expressivity, as the only processes allowed are tree-structured. Dardha and Gay define Priority CP (PCP), which allows cyclic-structured processes and restores deadlock freedom by using priorities, in line with Kobayashi and Padovani. Following PCP, we present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning. Consequently, we type cyclic-structured processes and restore deadlock freedom by using priorities. We show that our type system is sound by proving subject reduction and progress. We define an encoding from PCP to PGV and prove that the encoding preserves typing and is sound and complete with respect to the operational semantics.


    Volume: Volume 19, Issue 4
    Published on: December 18, 2023
    Accepted on: September 18, 2023
    Submitted on: December 18, 2021
    Keywords: Computer Science - Programming Languages
    Funding:
      Source : OpenAIRE Graph
    • Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233

    Consultation statistics

    This page has been seen 1045 times.
    This article's PDF has been downloaded 185 times.