# 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.
Keywords :
Document type :
Conference papers
Domain :

Cited literature [16 references]

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

### 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⟩

Record views