Journal article
Towards Races in Linear Logic
Logical methods in computer science, Vol.16(4), pp.1-16
09/29/2019
DOI: 10.23638/LMCS-16(4:15)2020
Abstract
Logical Methods in Computer Science, Volume 16, Issue 4 (December
15, 2020) lmcs:6979 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.
Details
- Title: Subtitle
- Towards Races in Linear Logic
- Creators
- Wen Kokke - University of EdinburghJ. Garrett Morris - University of EdinburghPhilip Wadler - University of Kansas
- Resource Type
- Journal article
- Publication Details
- Logical methods in computer science, Vol.16(4), pp.1-16
- DOI
- 10.23638/LMCS-16(4:15)2020
- ISSN
- 1860-5974
- eISSN
- 1860-5974
- Language
- English
- Date published
- 09/29/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259427202771
Metrics
8 Record Views