Wen Kokke ; J. Garrett Morris ; Philip Wadler - Towards Races in Linear Logic

lmcs:5821 - Logical Methods in Computer Science, December 15, 2020, Volume 16, Issue 4 - https://doi.org/10.23638/LMCS-16(4:15)2020
Towards Races in Linear LogicArticle

Authors: Wen Kokke ; J. Garrett Morris ; Philip Wadler

    Process calculi based in logic, such as $\pi$DILL and CP, provide a foundation for deadlock-free concurrent programming, but exclude non-determinism and races. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel composition from the $\pi$-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP. We introduce non-deterministic HCP, which extends HCP with a novel account of non-determinism. Our approach draws on bounded linear logic to provide a strongly-typed account of standard process calculus expressions of non-determinism. We show that our extension is expressive enough to capture many uses of non-determinism in untyped calculi, such as non-deterministic choice, while preserving HCP's meta-theoretic properties, including deadlock freedom.


    Volume: Volume 16, Issue 4
    Published on: December 15, 2020
    Accepted on: October 24, 2020
    Submitted on: October 9, 2019
    Keywords: Computer Science - Logic in Computer Science

    1 Document citing this article

    Consultation statistics

    This page has been seen 1945 times.
    This article's PDF has been downloaded 539 times.