Skip to Main content Skip to Navigation
Conference papers

Towards Races in Linear Logic

Abstract : 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 HCP${-} _{\text {ND}}$, 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.
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-02365505
Contributor : Hal Ifip <>
Submitted on : Friday, November 15, 2019 - 2:13:24 PM
Last modification on : Friday, November 15, 2019 - 2:29:54 PM
Long-term archiving on: : Sunday, February 16, 2020 - 5:06:21 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Wen Kokke, J. Morris, Philip Wadler. Towards Races in Linear Logic. 21th International Conference on Coordination Languages and Models (COORDINATION), Jun 2019, Kongens Lyngby, Denmark. pp.37-53, ⟨10.1007/978-3-030-22397-7_3⟩. ⟨hal-02365505⟩

Share

Metrics

Record views

68