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

TL;DR
This paper introduces non-deterministic HCP, extending linear logic-based process calculi to include non-determinism and races while maintaining deadlock freedom and strong typing.
Contribution
It presents a novel extension of HCP with non-determinism using bounded linear logic, addressing a key shortcoming in existing logic-based process calculi.
Findings
Captures non-deterministic choice in process calculus
Preserves deadlock freedom in the extended calculus
Provides a strongly-typed framework for non-deterministic processes
Abstract
Process calculi based in logic, such as 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 -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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
